src/HOL/Library/Quadratic_Discriminant.thy
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