diff -r 29235951f104 -r 333998becebe src/HOL/Library/Quadratic_Discriminant.thy --- a/src/HOL/Library/Quadratic_Discriminant.thy Thu Jun 28 17:14:52 2018 +0200 +++ b/src/HOL/Library/Quadratic_Discriminant.thy Sun Jul 01 10:58:14 2018 +0200 @@ -14,18 +14,8 @@ where "discrim a b c \ b\<^sup>2 - 4 * a * c" lemma complete_square: - fixes a b c x :: "real" - assumes "a \ 0" - shows "a * x\<^sup>2 + b * x + c = 0 \ (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 \a \ 0\ - have "a * x\<^sup>2 + b * x + c = 0 \ 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 \ (2 * a * x + b)\<^sup>2 = discrim a b c" - by (simp add: discrim_def power2_eq_square algebra_simps) -qed + "a \ 0 \ a * x\<^sup>2 + b * x + c = 0 \ (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 \ \" "b \ \" "a \ 0" + and "a*x^2 + b*x + c = 0" + and "sqrt (discrim a b c) \ \" + shows "x \ \" +using assms(1,2,5) discriminant_iff[THEN iffD1, OF assms(3,4)] by auto + +lemma Rats_solution_QE_converse: + assumes "a \ \" "b \ \" + and "a*x^2 + b*x + c = 0" + and "x \ \" + shows "sqrt (discrim a b c) \ \" +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) = \2*a*x+b\" by (simp) + thus ?thesis using \a \ \\ \b \ \\ \x \ \\ by (simp) +qed + end