author nipkow Sun, 01 Jul 2018 17:38:08 +0200 changeset 68555 5273df52ad83 parent 68552 391e89e03eef (current diff) parent 68554 333998becebe (diff) child 68556 fcffdcb8f506
merged
```--- a/src/HOL/Library/Quadratic_Discriminant.thy	Sat Jun 30 18:58:13 2018 +0100
+++ b/src/HOL/Library/Quadratic_Discriminant.thy	Sun Jul 01 17:38:08 2018 +0200
@@ -14,18 +14,8 @@
where "discrim a b c \<equiv> b\<^sup>2 - 4 * a * c"

lemma complete_square:
-  fixes a b c x :: "real"
-  assumes "a \<noteq> 0"
-  shows "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
-proof -
-  have "4 * a\<^sup>2 * x\<^sup>2 + 4 * a * b * x + 4 * a * c = 4 * a * (a * x\<^sup>2 + b * x + c)"
-    by (simp add: algebra_simps power2_eq_square)
-  with \<open>a \<noteq> 0\<close>
-  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"
-    by simp
-  then show "a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"
-    by (simp add: discrim_def power2_eq_square algebra_simps)
-qed
+  "a \<noteq> 0 \<Longrightarrow> a * x\<^sup>2 + b * x + c = 0 \<longleftrightarrow> (2 * a * x + b)\<^sup>2 = discrim a b c"

lemma discriminant_negative:
fixes a b c x :: real
@@ -190,4 +180,22 @@
qed
qed

+lemma Rats_solution_QE:
+  assumes "a \<in> \<rat>" "b \<in> \<rat>" "a \<noteq> 0"
+  and "a*x^2 + b*x + c = 0"
+  and "sqrt (discrim a b c) \<in> \<rat>"
+  shows "x \<in> \<rat>"
+using assms(1,2,5) discriminant_iff[THEN iffD1, OF assms(3,4)] by auto
+
+lemma Rats_solution_QE_converse:
+  assumes "a \<in> \<rat>" "b \<in> \<rat>"
+  and "a*x^2 + b*x + c = 0"
+  and "x \<in> \<rat>"
+  shows "sqrt (discrim a b c) \<in> \<rat>"
+proof -
+  from assms(3) have "discrim a b c = (2*a*x+b)^2" unfolding discrim_def by algebra
+  hence "sqrt (discrim a b c) = \<bar>2*a*x+b\<bar>" by (simp)
+  thus ?thesis using \<open>a \<in> \<rat>\<close> \<open>b \<in> \<rat>\<close> \<open>x \<in> \<rat>\<close> by (simp)
+qed
+
end```