author nipkow Sun Jul 01 17:38:08 2018 +0200 (11 months ago) changeset 68554 5273df52ad83 parent 68552 391e89e03eef parent 68553 333998becebe child 68556 fcffdcb8f506
merged
```     1.1 --- a/src/HOL/Library/Quadratic_Discriminant.thy	Sat Jun 30 18:58:13 2018 +0100
1.2 +++ b/src/HOL/Library/Quadratic_Discriminant.thy	Sun Jul 01 17:38:08 2018 +0200
1.3 @@ -14,18 +14,8 @@
1.4    where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"
1.5
1.6  lemma complete_square:
1.7 -  fixes a b c x :: "real"
1.8 -  assumes "a \<noteq> 0"
1.9 -  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
1.10 -proof -
1.11 -  have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
1.12 -    by (simp add: algebra_simps power2_eq_square)
1.13 -  with \<open>a \<noteq> 0\<close>
1.14 -  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.15 -    by simp
1.16 -  then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
1.17 -    by (simp add: discrim_def power2_eq_square algebra_simps)
1.18 -qed
1.19 +  "a \<noteq> 0 \<Longrightarrow> a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
1.20 +by (simp add: discrim_def) algebra
1.21
1.22  lemma discriminant_negative:
1.23    fixes a b c x :: real
1.24 @@ -190,4 +180,22 @@
1.25    qed
1.26  qed
1.27
1.28 +lemma Rats_solution_QE:
1.29 +  assumes "a \<in> \<rat>" "b \<in> \<rat>" "a \<noteq> 0"
1.30 +  and "a*x^2 + b*x + c = 0"
1.31 +  and "sqrt (discrim a b c) \<in> \<rat>"
1.32 +  shows "x \<in> \<rat>"
1.33 +using assms(1,2,5) discriminant_iff[THEN iffD1, OF assms(3,4)] by auto
1.34 +
1.35 +lemma Rats_solution_QE_converse:
1.36 +  assumes "a \<in> \<rat>" "b \<in> \<rat>"
1.37 +  and "a*x^2 + b*x + c = 0"
1.38 +  and "x \<in> \<rat>"
1.39 +  shows "sqrt (discrim a b c) \<in> \<rat>"
1.40 +proof -
1.41 +  from assms(3) have "discrim a b c = (2*a*x+b)^2" unfolding discrim_def by algebra
1.42 +  hence "sqrt (discrim a b c) = \<bar>2*a*x+b\<bar>" by (simp)
1.43 +  thus ?thesis using \<open>a \<in> \<rat>\<close> \<open>b \<in> \<rat>\<close> \<open>x \<in> \<rat>\<close> by (simp)
1.44 +qed
1.45 +
1.46  end
```