# HG changeset patch
# User nipkow
# Date 1530459488 -7200
# Node ID 5273df52ad830cadbf2c48d768d5ad7761144c1a
# Parent  391e89e03eef99743610d82b7e88051ac58e974e# Parent  333998becebe181ff1b2a3ccf16c95c79d734dbb
merged

diff -r 391e89e03eef -r 5273df52ad83 src/HOL/Library/Quadratic_Discriminant.thy
--- 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"
+by (simp add: discrim_def) algebra
 
 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