author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 60500 903bb1495239 child 62058 1cfd5d604937 permissions -rw-r--r--
more symbols;
```     1 (*  Title:       Roots of real quadratics
```
```     2     Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
```
```     3
```
```     4 Originally from the AFP entry Tarskis_Geometry
```
```     5 *)
```
```     6
```
```     7 section "Roots of real quadratics"
```
```     8
```
```     9 theory Quadratic_Discriminant
```
```    10 imports Complex_Main
```
```    11 begin
```
```    12
```
```    13 definition discrim :: "[real,real,real] \<Rightarrow> real" where
```
```    14   "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
```
```    15
```
```    16 lemma complete_square:
```
```    17   fixes a b c x :: "real"
```
```    18   assumes "a \<noteq> 0"
```
```    19   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
```
```    20 proof -
```
```    21   have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
```
```    22     by (simp add: algebra_simps power2_eq_square)
```
```    23   with \<open>a \<noteq> 0\<close>
```
```    24   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"
```
```    25     by simp
```
```    26   thus "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
```
```    27     unfolding discrim_def
```
```    28     by (simp add: power2_eq_square algebra_simps)
```
```    29 qed
```
```    30
```
```    31 lemma discriminant_negative:
```
```    32   fixes a b c x :: real
```
```    33   assumes "a \<noteq> 0"
```
```    34   and "discrim a b c < 0"
```
```    35   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
```
```    36 proof -
```
```    37   have "(2 * a * x + b)\<^sup>2 \<ge> 0" by simp
```
```    38   with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c" by arith
```
```    39   with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0" by simp
```
```    40 qed
```
```    41
```
```    42 lemma plus_or_minus_sqrt:
```
```    43   fixes x y :: real
```
```    44   assumes "y \<ge> 0"
```
```    45   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
```
```    46 proof
```
```    47   assume "x\<^sup>2 = y"
```
```    48   hence "sqrt (x\<^sup>2) = sqrt y" by simp
```
```    49   hence "sqrt y = \<bar>x\<bar>" by simp
```
```    50   thus "x = sqrt y \<or> x = - sqrt y" by auto
```
```    51 next
```
```    52   assume "x = sqrt y \<or> x = - sqrt y"
```
```    53   hence "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2" by auto
```
```    54   with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y" by simp
```
```    55 qed
```
```    56
```
```    57 lemma divide_non_zero:
```
```    58   fixes x y z :: real
```
```    59   assumes "x \<noteq> 0"
```
```    60   shows "x * y = z \<longleftrightarrow> y = z / x"
```
```    61 proof
```
```    62   assume "x * y = z"
```
```    63   with \<open>x \<noteq> 0\<close> show "y = z / x" by (simp add: field_simps)
```
```    64 next
```
```    65   assume "y = z / x"
```
```    66   with \<open>x \<noteq> 0\<close> show "x * y = z" by simp
```
```    67 qed
```
```    68
```
```    69 lemma discriminant_nonneg:
```
```    70   fixes a b c x :: real
```
```    71   assumes "a \<noteq> 0"
```
```    72   and "discrim a b c \<ge> 0"
```
```    73   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
```
```    74   x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```    75   x = (-b - sqrt (discrim a b c)) / (2 * a)"
```
```    76 proof -
```
```    77   from complete_square and plus_or_minus_sqrt and assms
```
```    78   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
```
```    79     (2 * a) * x + b = sqrt (discrim a b c) \<or>
```
```    80     (2 * a) * x + b = - sqrt (discrim a b c)"
```
```    81     by simp
```
```    82   also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
```
```    83     (2 * a) * x = (-b - sqrt (discrim a b c))"
```
```    84     by auto
```
```    85   also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
```
```    86   have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```    87     x = (-b - sqrt (discrim a b c)) / (2 * a)"
```
```    88     by simp
```
```    89   finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
```
```    90     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```    91     x = (-b - sqrt (discrim a b c)) / (2 * a)" .
```
```    92 qed
```
```    93
```
```    94 lemma discriminant_zero:
```
```    95   fixes a b c x :: real
```
```    96   assumes "a \<noteq> 0"
```
```    97   and "discrim a b c = 0"
```
```    98   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
```
```    99   using discriminant_nonneg and assms
```
```   100   by simp
```
```   101
```
```   102 theorem discriminant_iff:
```
```   103   fixes a b c x :: real
```
```   104   assumes "a \<noteq> 0"
```
```   105   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
```
```   106   discrim a b c \<ge> 0 \<and>
```
```   107   (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```   108   x = (-b - sqrt (discrim a b c)) / (2 * a))"
```
```   109 proof
```
```   110   assume "a * x\<^sup>2 + b * x + c = 0"
```
```   111   with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)" by auto
```
```   112   hence "discrim a b c \<ge> 0" by simp
```
```   113   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
```
```   114   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```   115     x = (-b - sqrt (discrim a b c)) / (2 * a)"
```
```   116     by simp
```
```   117   with \<open>discrim a b c \<ge> 0\<close>
```
```   118   show "discrim a b c \<ge> 0 \<and>
```
```   119     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```   120     x = (-b - sqrt (discrim a b c)) / (2 * a))" ..
```
```   121 next
```
```   122   assume "discrim a b c \<ge> 0 \<and>
```
```   123     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```   124     x = (-b - sqrt (discrim a b c)) / (2 * a))"
```
```   125   hence "discrim a b c \<ge> 0" and
```
```   126     "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
```
```   127     x = (-b - sqrt (discrim a b c)) / (2 * a)"
```
```   128     by simp_all
```
```   129   with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0" by simp
```
```   130 qed
```
```   131
```
```   132 lemma discriminant_nonneg_ex:
```
```   133   fixes a b c :: real
```
```   134   assumes "a \<noteq> 0"
```
```   135   and "discrim a b c \<ge> 0"
```
```   136   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
```
```   137   using discriminant_nonneg and assms
```
```   138   by auto
```
```   139
```
```   140 lemma discriminant_pos_ex:
```
```   141   fixes a b c :: real
```
```   142   assumes "a \<noteq> 0"
```
```   143   and "discrim a b c > 0"
```
```   144   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"
```
```   145 proof -
```
```   146   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
```
```   147   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
```
```   148   from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0" by simp
```
```   149   hence "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)" by arith
```
```   150   with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y" by simp
```
```   151   moreover
```
```   152   from discriminant_nonneg [of a b c ?x]
```
```   153     and discriminant_nonneg [of a b c ?y]
```
```   154     and assms
```
```   155   have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0" by simp_all
```
```   156   ultimately
```
```   157   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
```
```   158 qed
```
```   159
```
```   160 lemma discriminant_pos_distinct:
```
```   161   fixes a b c x :: real
```
```   162   assumes "a \<noteq> 0" and "discrim a b c > 0"
```
```   163   shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
```
```   164 proof -
```
```   165   from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
```
```   166   obtain w and z where "w \<noteq> z"
```
```   167     and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
```
```   168     by blast
```
```   169   show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
```
```   170   proof cases
```
```   171     assume "x = w"
```
```   172     with \<open>w \<noteq> z\<close> have "x \<noteq> z" by simp
```
```   173     with \<open>a * z\<^sup>2 + b * z + c = 0\<close>
```
```   174     show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
```
```   175   next
```
```   176     assume "x \<noteq> w"
```
```   177     with \<open>a * w\<^sup>2 + b * w + c = 0\<close>
```
```   178     show "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0" by auto
```
```   179   qed
```
```   180 qed
```
```   181
```
```   182 end
```