merged
authornipkow
Sun Jul 01 17:38:08 2018 +0200 (9 months ago)
changeset 685545273df52ad83
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