changeset 63465 d7610beb98bc parent 62058 1cfd5d604937 child 68553 333998becebe
```     1.1 --- a/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 19:12:17 2016 +0200
1.2 +++ b/src/HOL/Library/Quadratic_Discriminant.thy	Tue Jul 12 20:03:18 2016 +0200
1.3 @@ -10,8 +10,8 @@
1.4  imports Complex_Main
1.5  begin
1.6
1.7 -definition discrim :: "[real,real,real] \<Rightarrow> real" where
1.8 -  "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
1.9 +definition discrim :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
1.10 +  where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
1.11
1.12  lemma complete_square:
1.13    fixes a b c x :: "real"
1.14 @@ -23,20 +23,22 @@
1.15    with \<open>a \<noteq> 0\<close>
1.16    have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> 4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 0"
1.17      by simp
1.18 -  thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
1.19 -    unfolding discrim_def
1.20 -    by (simp add: power2_eq_square algebra_simps)
1.21 +  then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
1.22 +    by (simp add: discrim_def power2_eq_square algebra_simps)
1.23  qed
1.24
1.25  lemma discriminant_negative:
1.26    fixes a b c x :: real
1.27    assumes "a \<noteq> 0"
1.28 -  and "discrim a b c < 0"
1.29 +    and "discrim a b c < 0"
1.30    shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
1.31  proof -
1.32 -  have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
1.33 -  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
1.34 -  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
1.35 +  have "(2 * a * x + b)\<^sup>2 \<ge> 0"
1.36 +    by simp
1.37 +  with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
1.38 +    by arith
1.39 +  with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
1.40 +    by simp
1.41  qed
1.42
1.43  lemma plus_or_minus_sqrt:
1.44 @@ -45,13 +47,18 @@
1.45    shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
1.46  proof
1.47    assume "x\<^sup>2 = y"
1.48 -  hence "sqrt (x\<^sup>2) = sqrt y" by simp
1.49 -  hence "sqrt y = \<bar>x\<bar>" by simp
1.50 -  thus "x = sqrt y \<or> x = - sqrt y" by auto
1.51 +  then have "sqrt (x\<^sup>2) = sqrt y"
1.52 +    by simp
1.53 +  then have "sqrt y = \<bar>x\<bar>"
1.54 +    by simp
1.55 +  then show "x = sqrt y \<or> x = - sqrt y"
1.56 +    by auto
1.57  next
1.58    assume "x = sqrt y \<or> x = - sqrt y"
1.59 -  hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
1.60 -  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
1.61 +  then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
1.62 +    by auto
1.63 +  with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
1.64 +    by simp
1.65  qed
1.66
1.67  lemma divide_non_zero:
1.68 @@ -59,20 +66,19 @@
1.69    assumes "x \<noteq> 0"
1.70    shows "x * y = z \<longleftrightarrow> y = z / x"
1.71  proof
1.72 -  assume "x * y = z"
1.73 -  with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
1.74 -next
1.75 -  assume "y = z / x"
1.76 -  with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
1.77 +  show "y = z / x" if "x * y = z"
1.78 +    using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
1.79 +  show "x * y = z" if "y = z / x"
1.80 +    using \<open>x \<noteq> 0\<close> that by simp
1.81  qed
1.82
1.83  lemma discriminant_nonneg:
1.84    fixes a b c x :: real
1.85    assumes "a \<noteq> 0"
1.86 -  and "discrim a b c \<ge> 0"
1.87 +    and "discrim a b c \<ge> 0"
1.88    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
1.89 -  x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.90 -  x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.91 +    x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.92 +    x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.93  proof -
1.94    from complete_square and plus_or_minus_sqrt and assms
1.95    have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
1.96 @@ -94,88 +100,93 @@
1.97  lemma discriminant_zero:
1.98    fixes a b c x :: real
1.99    assumes "a \<noteq> 0"
1.100 -  and "discrim a b c = 0"
1.101 +    and "discrim a b c = 0"
1.102    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
1.103 -  using discriminant_nonneg and assms
1.104 -  by simp
1.105 +  by (simp add: discriminant_nonneg assms)
1.106
1.107  theorem discriminant_iff:
1.108    fixes a b c x :: real
1.109    assumes "a \<noteq> 0"
1.110    shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
1.111 -  discrim a b c \<ge> 0 \<and>
1.112 -  (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.113 -  x = (-b - sqrt (discrim a b c)) / (2 * a))"
1.114 +    discrim a b c \<ge> 0 \<and>
1.115 +    (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.116 +     x = (-b - sqrt (discrim a b c)) / (2 * a))"
1.117  proof
1.118    assume "a * x\<^sup>2 + b * x + c = 0"
1.119 -  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
1.120 -  hence "discrim a b c \<ge> 0" by simp
1.121 +  with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
1.122 +    by auto
1.123 +  then have "discrim a b c \<ge> 0"
1.124 +    by simp
1.125    with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
1.126    have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.127 -    x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.128 +      x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.129      by simp
1.130    with \<open>discrim a b c \<ge> 0\<close>
1.131    show "discrim a b c \<ge> 0 \<and>
1.132      (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.133 -    x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
1.134 +     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
1.135  next
1.136    assume "discrim a b c \<ge> 0 \<and>
1.137      (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.138 -    x = (-b - sqrt (discrim a b c)) / (2 * a))"
1.139 -  hence "discrim a b c \<ge> 0" and
1.140 +     x = (-b - sqrt (discrim a b c)) / (2 * a))"
1.141 +  then have "discrim a b c \<ge> 0" and
1.142      "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
1.143 -    x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.144 +     x = (-b - sqrt (discrim a b c)) / (2 * a)"
1.145      by simp_all
1.146 -  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
1.147 +  with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
1.148 +    by simp
1.149  qed
1.150
1.151  lemma discriminant_nonneg_ex:
1.152    fixes a b c :: real
1.153    assumes "a \<noteq> 0"
1.154 -  and "discrim a b c \<ge> 0"
1.155 +    and "discrim a b c \<ge> 0"
1.156    shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
1.157 -  using discriminant_nonneg and assms
1.158 -  by auto
1.159 +  by (auto simp: discriminant_nonneg assms)
1.160
1.161  lemma discriminant_pos_ex:
1.162    fixes a b c :: real
1.163    assumes "a \<noteq> 0"
1.164 -  and "discrim a b c > 0"
1.165 -  shows "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
1.166 +    and "discrim a b c > 0"
1.167 +  shows "\<exists>x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0"
1.168  proof -
1.169    let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
1.170    let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
1.171 -  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
1.172 -  hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
1.173 -  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
1.174 -  moreover
1.175 -  from discriminant_nonneg [of a b c ?x]
1.176 -    and discriminant_nonneg [of a b c ?y]
1.177 -    and assms
1.178 -  have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
1.179 -  ultimately
1.180 -  show "\<exists> x y. x \<noteq> y \<and> a * x\<^sup>2 + b * x + c = 0 \<and> a * y\<^sup>2 + b * y + c = 0" by blast
1.181 +  from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
1.182 +    by simp
1.183 +  then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
1.184 +    by arith
1.185 +  with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
1.186 +    by simp
1.187 +  moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
1.188 +    using discriminant_nonneg [of a b c ?x]
1.189 +      and discriminant_nonneg [of a b c ?y]
1.190 +    by simp_all
1.191 +  ultimately show ?thesis
1.192 +    by blast
1.193  qed
1.194
1.195  lemma discriminant_pos_distinct:
1.196    fixes a b c x :: real
1.197 -  assumes "a \<noteq> 0" and "discrim a b c > 0"
1.198 +  assumes "a \<noteq> 0"
1.199 +    and "discrim a b c > 0"
1.200    shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
1.201  proof -
1.202    from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
1.203    obtain w and z where "w \<noteq> z"
1.204      and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
1.205      by blast
1.206 -  show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
1.207 -  proof cases
1.208 -    assume "x = w"
1.209 -    with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
1.210 -    with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
1.211 -    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
1.212 +  show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
1.213 +  proof (cases "x = w")
1.214 +    case True
1.215 +    with \<open>w \<noteq> z\<close> have "x \<noteq> z"
1.216 +      by simp
1.217 +    with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
1.218 +      by auto
1.219    next
1.220 -    assume "x \<noteq> w"
1.221 -    with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
1.222 -    show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
1.223 +    case False
1.224 +    with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
1.225 +      by auto
1.226    qed
1.227  qed
1.228
```