author Manuel Eberl Mon Mar 26 16:14:16 2018 +0200 (18 months ago) changeset 67951 655aa11359dc parent 63465 d7610beb98bc child 68553 333998becebe permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
1 (*  Title:       HOL/Library/Quadratic_Discriminant.thy
2     Author:      Tim Makarios <tjm1983 at gmail.com>, 2012
4 Originally from the AFP entry Tarskis_Geometry
5 *)
7 section "Roots of real quadratics"
10 imports Complex_Main
11 begin
13 definition discrim :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
14   where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
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   then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
27     by (simp add: discrim_def power2_eq_square algebra_simps)
28 qed
30 lemma discriminant_negative:
31   fixes a b c x :: real
32   assumes "a \<noteq> 0"
33     and "discrim a b c < 0"
34   shows "a * x\<^sup>2 + b * x + c \<noteq> 0"
35 proof -
36   have "(2 * a * x + b)\<^sup>2 \<ge> 0"
37     by simp
38   with \<open>discrim a b c < 0\<close> have "(2 * a * x + b)\<^sup>2 \<noteq> discrim a b c"
39     by arith
40   with complete_square and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c \<noteq> 0"
41     by simp
42 qed
44 lemma plus_or_minus_sqrt:
45   fixes x y :: real
46   assumes "y \<ge> 0"
47   shows "x\<^sup>2 = y \<longleftrightarrow> x = sqrt y \<or> x = - sqrt y"
48 proof
49   assume "x\<^sup>2 = y"
50   then have "sqrt (x\<^sup>2) = sqrt y"
51     by simp
52   then have "sqrt y = \<bar>x\<bar>"
53     by simp
54   then show "x = sqrt y \<or> x = - sqrt y"
55     by auto
56 next
57   assume "x = sqrt y \<or> x = - sqrt y"
58   then have "x\<^sup>2 = (sqrt y)\<^sup>2 \<or> x\<^sup>2 = (- sqrt y)\<^sup>2"
59     by auto
60   with \<open>y \<ge> 0\<close> show "x\<^sup>2 = y"
61     by simp
62 qed
64 lemma divide_non_zero:
65   fixes x y z :: real
66   assumes "x \<noteq> 0"
67   shows "x * y = z \<longleftrightarrow> y = z / x"
68 proof
69   show "y = z / x" if "x * y = z"
70     using \<open>x \<noteq> 0\<close> that by (simp add: field_simps)
71   show "x * y = z" if "y = z / x"
72     using \<open>x \<noteq> 0\<close> that by simp
73 qed
75 lemma discriminant_nonneg:
76   fixes a b c x :: real
77   assumes "a \<noteq> 0"
78     and "discrim a b c \<ge> 0"
79   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
80     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
81     x = (-b - sqrt (discrim a b c)) / (2 * a)"
82 proof -
83   from complete_square and plus_or_minus_sqrt and assms
84   have "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
85     (2 * a) * x + b = sqrt (discrim a b c) \<or>
86     (2 * a) * x + b = - sqrt (discrim a b c)"
87     by simp
88   also have "\<dots> \<longleftrightarrow> (2 * a) * x = (-b + sqrt (discrim a b c)) \<or>
89     (2 * a) * x = (-b - sqrt (discrim a b c))"
90     by auto
91   also from \<open>a \<noteq> 0\<close> and divide_non_zero [of "2 * a" x]
92   have "\<dots> \<longleftrightarrow> x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
93     x = (-b - sqrt (discrim a b c)) / (2 * a)"
94     by simp
95   finally show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
96     x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
97     x = (-b - sqrt (discrim a b c)) / (2 * a)" .
98 qed
100 lemma discriminant_zero:
101   fixes a b c x :: real
102   assumes "a \<noteq> 0"
103     and "discrim a b c = 0"
104   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> x = -b / (2 * a)"
105   by (simp add: discriminant_nonneg assms)
107 theorem discriminant_iff:
108   fixes a b c x :: real
109   assumes "a \<noteq> 0"
110   shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow>
111     discrim a b c \<ge> 0 \<and>
112     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
113      x = (-b - sqrt (discrim a b c)) / (2 * a))"
114 proof
115   assume "a * x\<^sup>2 + b * x + c = 0"
116   with discriminant_negative and \<open>a \<noteq> 0\<close> have "\<not>(discrim a b c < 0)"
117     by auto
118   then have "discrim a b c \<ge> 0"
119     by simp
120   with discriminant_nonneg and \<open>a * x\<^sup>2 + b * x + c = 0\<close> and \<open>a \<noteq> 0\<close>
121   have "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
122       x = (-b - sqrt (discrim a b c)) / (2 * a)"
123     by simp
124   with \<open>discrim a b c \<ge> 0\<close>
125   show "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 next
129   assume "discrim a b c \<ge> 0 \<and>
130     (x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
131      x = (-b - sqrt (discrim a b c)) / (2 * a))"
132   then have "discrim a b c \<ge> 0" and
133     "x = (-b + sqrt (discrim a b c)) / (2 * a) \<or>
134      x = (-b - sqrt (discrim a b c)) / (2 * a)"
135     by simp_all
136   with discriminant_nonneg and \<open>a \<noteq> 0\<close> show "a * x\<^sup>2 + b * x + c = 0"
137     by simp
138 qed
140 lemma discriminant_nonneg_ex:
141   fixes a b c :: real
142   assumes "a \<noteq> 0"
143     and "discrim a b c \<ge> 0"
144   shows "\<exists> x. a * x\<^sup>2 + b * x + c = 0"
145   by (auto simp: discriminant_nonneg assms)
147 lemma discriminant_pos_ex:
148   fixes a b c :: real
149   assumes "a \<noteq> 0"
150     and "discrim a b c > 0"
151   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"
152 proof -
153   let ?x = "(-b + sqrt (discrim a b c)) / (2 * a)"
154   let ?y = "(-b - sqrt (discrim a b c)) / (2 * a)"
155   from \<open>discrim a b c > 0\<close> have "sqrt (discrim a b c) \<noteq> 0"
156     by simp
157   then have "sqrt (discrim a b c) \<noteq> - sqrt (discrim a b c)"
158     by arith
159   with \<open>a \<noteq> 0\<close> have "?x \<noteq> ?y"
160     by simp
161   moreover from assms have "a * ?x\<^sup>2 + b * ?x + c = 0" and "a * ?y\<^sup>2 + b * ?y + c = 0"
162     using discriminant_nonneg [of a b c ?x]
163       and discriminant_nonneg [of a b c ?y]
164     by simp_all
165   ultimately show ?thesis
166     by blast
167 qed
169 lemma discriminant_pos_distinct:
170   fixes a b c x :: real
171   assumes "a \<noteq> 0"
172     and "discrim a b c > 0"
173   shows "\<exists> y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
174 proof -
175   from discriminant_pos_ex and \<open>a \<noteq> 0\<close> and \<open>discrim a b c > 0\<close>
176   obtain w and z where "w \<noteq> z"
177     and "a * w\<^sup>2 + b * w + c = 0" and "a * z\<^sup>2 + b * z + c = 0"
178     by blast
179   show "\<exists>y. x \<noteq> y \<and> a * y\<^sup>2 + b * y + c = 0"
180   proof (cases "x = w")
181     case True
182     with \<open>w \<noteq> z\<close> have "x \<noteq> z"
183       by simp
184     with \<open>a * z\<^sup>2 + b * z + c = 0\<close> show ?thesis
185       by auto
186   next
187     case False
188     with \<open>a * w\<^sup>2 + b * w + c = 0\<close> show ?thesis
189       by auto
190   qed
191 qed
193 end