# HG changeset patch # User kleing # Date 1419741754 -39600 # Node ID 3a594fd13ca4ff44359d44812040b8707c72957e # Parent ad8e0a789af6ab8191675f706adbea3e1dd8b38e 3 old example lemmas by Amine listed in the top 100 theorems diff -r ad8e0a789af6 -r 3a594fd13ca4 src/HOL/ROOT --- a/src/HOL/ROOT Sat Dec 27 20:32:06 2014 +0100 +++ b/src/HOL/ROOT Sun Dec 28 15:42:34 2014 +1100 @@ -559,6 +559,8 @@ PER NatSum ThreeDivides + Cubic_Quartic + Pythagoras Intuitionistic CTL Arith_Examples diff -r ad8e0a789af6 -r 3a594fd13ca4 src/HOL/ex/Cubic_Quartic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Cubic_Quartic.thy Sun Dec 28 15:42:34 2014 +1100 @@ -0,0 +1,145 @@ +(* Title: HOL/ex/Cubic_Quartic.thy + Author: Amine Chaieb +*) + +header "The Cubic and Quartic Root Formulas" + +theory Cubic_Quartic +imports Complex_Main +begin + +section "The Cubic Formula" + +definition "ccbrt z = (SOME (w::complex). w^3 = z)" + +lemma ccbrt: "(ccbrt z) ^ 3 = z" +proof- + from rcis_Ex obtain r a where ra: "z = rcis r a" by blast + let ?r' = "if r < 0 then - root 3 (-r) else root 3 r" + let ?a' = "a/3" + have "rcis ?r' ?a' ^ 3 = rcis r a" by (cases "r<0", simp_all add: DeMoivre2) + hence th: "\w. w^3 = z" unfolding ra by blast + from someI_ex[OF th] show ?thesis unfolding ccbrt_def by blast +qed + +text "The reduction to a simpler form:" + +lemma cubic_reduction: + fixes a :: complex + assumes H: "a \ 0 \ x = y - b / (3 * a) \ p = (3* a * c - b^2) / (9 * a^2) \ + q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)" + shows "a * x^3 + b * x^2 + c * x + d = 0 \ y^3 + 3 * p * y - 2 * q = 0" +proof- + from H have "3*a \ 0" "9*a^2 \ 0" "54*a^3 \ 0" by auto + hence th: "x = y - b / (3 * a) \ (3*a) * x = (3*a) * y - b" + "p = (3* a * c - b^2) / (9 * a^2) \ (9 * a^2) * p = (3* a * c - b^2)" + "q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3) \ + (54 * a^3) * q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d)" + by (simp_all add: field_simps) + from H[unfolded th] show ?thesis by algebra +qed + +text "The solutions of the special form:" + +lemma cubic_basic: + fixes s :: complex + assumes H: "s^2 = q^2 + p^3 \ + s1^3 = (if p = 0 then 2 * q else q + s) \ + s2 = -s1 * (1 + i * t) / 2 \ + s3 = -s1 * (1 - i * t) / 2 \ + i^2 + 1 = 0 \ + t^2 = 3" + shows + "if p = 0 + then y^3 + 3 * p * y - 2 * q = 0 \ y = s1 \ y = s2 \ y = s3 + else s1 \ 0 \ + (y^3 + 3 * p * y - 2 * q = 0 \ (y = s1 - p / s1 \ y = s2 - p / s2 \ y = s3 - p / s3))" +proof- + { assume p0: "p = 0" + with H have ?thesis by (simp add: field_simps) algebra + } + moreover + { assume p0: "p \ 0" + with H have th1: "s1 \ 0" by (simp add: field_simps) algebra + from p0 H th1 have th0: "s2 \ 0" "s3 \0" + by (simp_all add: field_simps) algebra+ + from th1 th0 + have th: "y = s1 - p / s1 \ s1*y = s1^2 - p" + "y = s2 - p / s2 \ s2*y = s2^2 - p" + "y = s3 - p / s3 \ s3*y = s3^2 - p" + by (simp_all add: field_simps power2_eq_square) + from p0 H have ?thesis unfolding th by (simp add: field_simps) algebra + } + ultimately show ?thesis by blast +qed + +text "Explicit formula for the roots:" + +lemma cubic: + assumes a0: "a \ 0" + shows " + let p = (3 * a * c - b^2) / (9 * a^2) ; + q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3); + s = csqrt(q^2 + p^3); + s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s)); + s2 = -s1 * (1 + ii * csqrt 3) / 2; + s3 = -s1 * (1 - ii * csqrt 3) / 2 + in if p = 0 then + a * x^3 + b * x^2 + c * x + d = 0 \ + x = s1 - b / (3 * a) \ + x = s2 - b / (3 * a) \ + x = s3 - b / (3 * a) + else + s1 \ 0 \ + (a * x^3 + b * x^2 + c * x + d = 0 \ + x = s1 - p / s1 - b / (3 * a) \ + x = s2 - p / s2 - b / (3 * a) \ + x = s3 - p / s3 - b / (3 * a))" +proof- + let ?p = "(3 * a * c - b^2) / (9 * a^2)" + let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)" + let ?s = "csqrt(?q^2 + ?p^3)" + let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)" + let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2" + let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2" + let ?y = "x + b / (3 * a)" + from a0 have zero: "9 * a^2 \ 0" "a^3 * 54 \ 0" "(a*3)\ 0" by auto + have eq:"a * x^3 + b * x^2 + c * x + d = 0 \ ?y^3 + 3 * ?p * ?y - 2 * ?q = 0" + by (rule cubic_reduction) (auto simp add: field_simps zero a0) + have "csqrt 3^2 = 3" by (rule power2_csqrt) + hence th0: "?s^2 = ?q^2 + ?p ^ 3 \ ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \ + ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \ + ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \ + ii^2 + 1 = 0 \ csqrt 3^2 = 3" + using zero by (simp add: field_simps power2_csqrt ccbrt) + from cubic_basic[OF th0, of ?y] + show ?thesis + apply (simp only: Let_def eq) + using zero apply (simp add: field_simps ccbrt power2_csqrt) + using zero + apply (cases "a * (c * 3) = b^2", simp_all add: field_simps) + done +qed + + +section "The Quartic Formula" + +lemma quartic: + "(y::real)^3 - b * y^2 + (a * c - 4 * d) * y - a^2 * d + 4 * b * d - c^2 = 0 \ + R^2 = a^2 / 4 - b + y \ + s^2 = y^2 - 4 * d \ + (D^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b + 2 * s + else 3 * a^2 / 4 - R^2 - 2 * b + (4 * a * b - 8 * c - a^3) / (4 * R))) \ + (E^2 = (if R = 0 then 3 * a^2 / 4 - 2 * b - 2 * s + else 3 * a^2 / 4 - R^2 - 2 * b - (4 * a * b - 8 * c - a^3) / (4 * R))) + \ x^4 + a * x^3 + b * x^2 + c * x + d = 0 \ + x = -a / 4 + R / 2 + D / 2 \ + x = -a / 4 + R / 2 - D / 2 \ + x = -a / 4 - R / 2 + E / 2 \ + x = -a / 4 - R / 2 - E / 2" +apply (cases "R=0", simp_all add: field_simps divide_minus_left[symmetric] del: divide_minus_left) + apply algebra +apply algebra +done + +end \ No newline at end of file diff -r ad8e0a789af6 -r 3a594fd13ca4 src/HOL/ex/Pythagoras.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Pythagoras.thy Sun Dec 28 15:42:34 2014 +1100 @@ -0,0 +1,32 @@ +(* Title: HOL/ex/Pythagoras.thy + Author: Amine Chaieb +*) + +header "The Pythagorean Theorem" + +theory Pythagoras +imports Complex_Main +begin + +text {* Expressed in real numbers: *} + +lemma pythagoras_verbose: + "((A1::real) - B1) * (C1 - B1) + (A2 - B2) * (C2 - B2) = 0 \ + (C1 - A1) * (C1 - A1) + (C2 - A2) * (C2 - A2) = + ((B1 - A1) * (B1 - A1) + (B2 - A2) * (B2 - A2)) + (C1 - B1) * (C1 - B1) + (C2 - B2) * (C2 - B2)" + by algebra + + +text {* Expressed in vectors: *} + +type_synonym point = "real \ real" + +lemma pythagoras: + defines ort:"orthogonal \ (\(A::point) B. fst A * fst B + snd A * snd B = 0)" + and vc:"vector \ (\(A::point) B. (fst A - fst B, snd A - snd B))" + and vcn:"vecsqnorm \ (\A::point. fst A ^ 2 + snd A ^2)" + assumes o: "orthogonal (vector A B) (vector C B)" + shows "vecsqnorm(vector C A) = vecsqnorm(vector B A) + vecsqnorm(vector C B)" + using o unfolding ort vc vcn by (algebra add: fst_conv snd_conv) + + end \ No newline at end of file