# HG changeset patch # User wenzelm # Date 1411414305 -7200 # Node ID b5d27faef560669405eb099b624dbc9b5c84275e # Parent fa50722ad6cbe7ce46580c919c5dfeb831b9710d# Parent 37cbbd8eb4603246a84cdd9f64bb5a14ac68731e merged diff -r fa50722ad6cb -r b5d27faef560 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Mon Sep 22 15:01:27 2014 +0200 +++ b/Admin/components/components.sha1 Mon Sep 22 21:31:45 2014 +0200 @@ -1,3 +1,4 @@ +70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz 842d9526f37b928cf9e22f141884365129990d63 cygwin-20130110.tar.gz cb3b0706d208f104b800267697204f6d82f7b48a cygwin-20130114.tar.gz diff -r fa50722ad6cb -r b5d27faef560 Admin/components/main --- a/Admin/components/main Mon Sep 22 15:01:27 2014 +0200 +++ b/Admin/components/main Mon Sep 22 21:31:45 2014 +0200 @@ -1,5 +1,6 @@ #main components for everyday use, without big impact on overall build time cvc3-2.4.1 +csdp-6.x e-1.8 exec_process-1.0.3 Haskabelle-2014 diff -r fa50722ad6cb -r b5d27faef560 NEWS --- a/NEWS Mon Sep 22 15:01:27 2014 +0200 +++ b/NEWS Mon Sep 22 21:31:45 2014 +0200 @@ -25,6 +25,10 @@ of numeral signs, particulary in expressions involving infix syntax like "(- 1) ^ n". +* Old inner token category "xnum" has been discontinued. Potential +INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num" +token category instead. + *** HOL *** diff -r fa50722ad6cb -r b5d27faef560 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 22 15:01:27 2014 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Mon Sep 22 21:31:45 2014 +0200 @@ -601,7 +601,6 @@ @{syntax_def (inner) tvar} & = & @{syntax_ref typevar} \\ @{syntax_def (inner) num_token} & = & @{syntax_ref nat} \\ @{syntax_def (inner) float_token} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\ - @{syntax_def (inner) xnum_token} & = & @{verbatim "#"}@{syntax_ref nat}@{text " | "}@{verbatim "#-"}@{syntax_ref nat} \\ @{syntax_def (inner) str_token} & = & @{verbatim "''"} @{text "\"} @{verbatim "''"} \\ @{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\"} @{verbatim "\""} \\ @{syntax_def (inner) cartouche} & = & @{verbatim "\"} @{text "\"} @{verbatim "\"} \\ @@ -609,17 +608,15 @@ \end{center} The token categories @{syntax (inner) num_token}, @{syntax (inner) - float_token}, @{syntax (inner) xnum_token}, @{syntax (inner) - str_token}, @{syntax (inner) string_token}, and @{syntax (inner) - cartouche} are not used in Pure. Object-logics may implement - numerals and string literals by adding appropriate syntax - declarations, together with some translation functions (e.g.\ see - @{file "~~/src/HOL/Tools/string_syntax.ML"}). + float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token}, + and @{syntax (inner) cartouche} are not used in Pure. Object-logics may + implement numerals and string literals by adding appropriate syntax + declarations, together with some translation functions (e.g.\ see @{file + "~~/src/HOL/Tools/string_syntax.ML"}). - The derived categories @{syntax_def (inner) num_const}, @{syntax_def - (inner) float_const}, and @{syntax_def (inner) xnum_const} provide - robust access to the respective tokens: the syntax tree holds a - syntactic constant instead of a free variable. + The derived categories @{syntax_def (inner) num_const}, and @{syntax_def + (inner) float_const}, provide robust access to the respective tokens: the + syntax tree holds a syntactic constant instead of a free variable. *} diff -r fa50722ad6cb -r b5d27faef560 src/HOL/Library/Sum_of_Squares.thy --- a/src/HOL/Library/Sum_of_Squares.thy Mon Sep 22 15:01:27 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares.thy Mon Sep 22 21:31:45 2014 +0200 @@ -38,130 +38,4 @@ the proof without calling an external prover. *} -setup SOS_Wrapper.setup - -text {* Tests *} - -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" -by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") - -lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" -by (sos_cert "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") - -lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" -by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") - -lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" -by (sos_cert "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") - -lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" -by (sos_cert "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") - -lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" -by (sos_cert "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") - -lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" -by (sos_cert "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") - -lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" -by (sos_cert "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") - -lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" -by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") - -lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" -by (sos_cert "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") - -(* ------------------------------------------------------------------------- *) -(* One component of denominator in dodecahedral example. *) -(* ------------------------------------------------------------------------- *) - -lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" -by (sos_cert "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") - -(* ------------------------------------------------------------------------- *) -(* Over a larger but simpler interval. *) -(* ------------------------------------------------------------------------- *) - -lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" -by (sos_cert "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") - -(* ------------------------------------------------------------------------- *) -(* We can do 12. I think 12 is a sharp bound; see PP's certificate. *) -(* ------------------------------------------------------------------------- *) - -lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" -by (sos_cert "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") - -(* ------------------------------------------------------------------------- *) -(* Inequality from sci.math (see "Leon-Sotelo, por favor"). *) -(* ------------------------------------------------------------------------- *) - -lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" -by (sos_cert "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") - -lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" -by (sos_cert "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") - -lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" -by (sos_cert "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") - -lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \ c * a^2 * b <= x" -by (sos_cert "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") - -lemma "(0::real) < x --> 0 < 1 + x + x^2" -by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") - -lemma "(0::real) <= x --> 0 < 1 + x + x^2" -by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") - -lemma "(0::real) < 1 + x^2" -by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") - -lemma "(0::real) <= 1 + 2 * x + x^2" -by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") - -lemma "(0::real) < 1 + abs x" -by (sos_cert "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") - -lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" -by (sos_cert "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") - - - -lemma "abs ((1::real) + x^2) = (1::real) + x^2" -by (sos_cert "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") -lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0" -by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") - -lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" -by (sos_cert "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") -lemma "(1::real) < x --> x^2 < y --> 1 < y" -by (sos_cert "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") -lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" -by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") -lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" -by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") -lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" -by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") -lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" -by (sos_cert "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") -lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" -by (sos_cert "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") - - -(* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) - -lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" -by (sos_cert "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") - -lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" -by (sos_cert "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") - -lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" -by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") - -lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" -by (sos_cert "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") - end diff -r fa50722ad6cb -r b5d27faef560 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Sep 22 15:01:27 2014 +0200 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Sep 22 21:31:45 2014 +0200 @@ -7,7 +7,6 @@ signature SOS_WRAPPER = sig datatype prover_result = Success | Failure | Error - val setup: theory -> theory val dest_dir: string Config.T val prover_name: string Config.T end @@ -139,8 +138,8 @@ fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method -val setup = - Method.setup @{binding sos} +val _ = Theory.setup + (Method.setup @{binding sos} (Scan.lift (Scan.option Parse.xname) >> (fn opt_name => fn ctxt => sos_solver print_cert @@ -151,6 +150,6 @@ >> (fn cert => fn ctxt => sos_solver ignore (Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt)) - "prove universal problems over the reals using sums of squares with certificates" + "prove universal problems over the reals using sums of squares with certificates") end diff -r fa50722ad6cb -r b5d27faef560 src/HOL/Num.thy --- a/src/HOL/Num.thy Mon Sep 22 15:01:27 2014 +0200 +++ b/src/HOL/Num.thy Mon Sep 22 21:31:45 2014 +0200 @@ -287,7 +287,7 @@ fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ numeral_tr [t] $ u | numeral_tr [Const (num, _)] = - (Numeral.mk_number_syntax o #value o Lexicon.read_xnum) num + (Numeral.mk_number_syntax o #value o Lexicon.read_num) num | numeral_tr ts = raise TERM ("numeral_tr", ts); in [(@{syntax_const "_Numeral"}, K numeral_tr)] end *} diff -r fa50722ad6cb -r b5d27faef560 src/HOL/ROOT --- a/src/HOL/ROOT Mon Sep 22 15:01:27 2014 +0200 +++ b/src/HOL/ROOT Mon Sep 22 21:31:45 2014 +0200 @@ -54,8 +54,6 @@ Old_Datatype Old_Recdef Old_SMT - theories [condition = ISABELLE_FULL_TEST] - Sum_of_Squares_Remote document_files "root.bib" "root.tex" session "HOL-Hahn_Banach" in Hahn_Banach = HOL + @@ -601,6 +599,11 @@ ML SAT_Examples Nominal2_Dummy + SOS_Cert + theories [condition = ISABELLE_CSDP] + SOS + theories [condition = ISABELLE_FULL_TEST] + SOS_Remote theories [skip_proofs = false] Meson_Test theories [condition = SVC_HOME] diff -r fa50722ad6cb -r b5d27faef560 src/HOL/ex/SOS.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SOS.thy Mon Sep 22 21:31:45 2014 +0200 @@ -0,0 +1,130 @@ +(* Title: HOL/ex/SOS.thy + Author: Amine Chaieb, University of Cambridge + Author: Philipp Meyer, TU Muenchen + +Examples for Sum_of_Squares. +*) + +theory SOS +imports "~~/src/HOL/Library/Sum_of_Squares" +begin + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" + by (sos csdp) + +lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" + by (sos csdp) + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" + by (sos csdp) + +lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" + by (sos csdp) + +lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" + by (sos csdp) + +lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" + by (sos csdp) + +lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" + by (sos csdp) + +lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" + by (sos csdp) + +lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" + by (sos csdp) + +lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" + by (sos csdp) + + +text \One component of denominator in dodecahedral example.\ + +lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" + by (sos csdp) + + +text \Over a larger but simpler interval.\ + +lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" + by (sos csdp) + + +text \We can do 12. I think 12 is a sharp bound; see PP's certificate.\ + +lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" + by (sos csdp) + + +text \Inequality from sci.math (see "Leon-Sotelo, por favor").\ + +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" + by (sos csdp) + +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" + by (sos csdp) + +lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" + by (sos csdp) + +lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \ c * a^2 * b <= x" + by (sos csdp) + +lemma "(0::real) < x --> 0 < 1 + x + x^2" + by (sos csdp) + +lemma "(0::real) <= x --> 0 < 1 + x + x^2" + by (sos csdp) + +lemma "(0::real) < 1 + x^2" + by (sos csdp) + +lemma "(0::real) <= 1 + 2 * x + x^2" + by (sos csdp) + +lemma "(0::real) < 1 + abs x" + by (sos csdp) + +lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" + by (sos csdp) + + +lemma "abs ((1::real) + x^2) = (1::real) + x^2" + by (sos csdp) +lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0" + by (sos csdp) + +lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" + by (sos csdp) +lemma "(1::real) < x --> x^2 < y --> 1 < y" + by (sos csdp) +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" + by (sos csdp) +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" + by (sos csdp) +lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" + by (sos csdp) +lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" + by (sos csdp) +lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" + by (sos csdp) + + +(* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) + +lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" + by (sos csdp) + +lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" + by (sos csdp) + +lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" + by (sos csdp) + +lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" + by (sos csdp) + +end + diff -r fa50722ad6cb -r b5d27faef560 src/HOL/ex/SOS_Cert.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SOS_Cert.thy Mon Sep 22 21:31:45 2014 +0200 @@ -0,0 +1,130 @@ +(* Title: HOL/ex/SOS_Cert.thy + Author: Amine Chaieb, University of Cambridge + Author: Philipp Meyer, TU Muenchen + +Examples for Sum_of_Squares: replay of certificates. +*) + +theory SOS_Cert +imports "~~/src/HOL/Library/Sum_of_Squares" +begin + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" + by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + +lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" + by (sos_cert "(((A<0 * R<1) + (([~1/2*a1*b2 + ~1/2*a2*b1] * A=0) + (([~1/2*a1*a2 + 1/2*b1*b2] * A=1) + (((A<0 * R<1) * ((R<1/2 * [b2]^2) + (R<1/2 * [b1]^2))) + ((A<=0 * (A<=1 * R<1)) * ((R<1/2 * [b2]^2) + ((R<1/2 * [b1]^2) + ((R<1/2 * [a2]^2) + (R<1/2 * [a1]^2))))))))))") + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" + by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + +lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" + by (sos_cert "((R<1 + (((A<=3 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=7 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=5 * R<1)) * (R<1 * [1]^2)))))))") + +lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" + by (sos_cert "(((A<0 * R<1) + (((A<0 * R<1) * (R<1/2 * [1]^2)) + (((A<=2 * R<1) * (R<1/2 * [~1*x + y]^2)) + (((A<=1 * R<1) * (R<1/2 * [~1*x + z]^2)) + (((A<=1 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + (((A<=0 * R<1) * (R<1/2 * [~1*y + z]^2)) + (((A<=0 * (A<=2 * (A<=3 * R<1))) * (R<1/2 * [1]^2)) + ((A<=0 * (A<=1 * (A<=3 * R<1))) * (R<1/2 * [1]^2))))))))))") + +lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" + by (sos_cert "(((A<0 * R<1) + (([~3] * A=0) + (R<1 * ((R<2 * [~1/2*x + ~1/2*y + z]^2) + (R<3/2 * [~1*x + y]^2))))))") + +lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" + by (sos_cert "(((A<0 * R<1) + (([~4] * A=0) + (R<1 * ((R<3 * [~1/3*w + ~1/3*x + ~1/3*y + z]^2) + ((R<8/3 * [~1/2*w + ~1/2*x + y]^2) + (R<2 * [~1*w + x]^2)))))))") + +lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" + by (sos_cert "(((A<0 * R<1) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))") + +lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" + by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * R<1) * (R<1 * [1]^2))))") + +lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" + by (sos_cert "((((A<0 * R<1) + ((A<=1 * R<1) * (R<1 * [~8*x^3 + ~4*x^2 + 4*x + 1]^2)))) & ((((A<0 * A<1) * R<1) + ((A<=1 * (A<0 * R<1)) * (R<1 * [8*x^3 + ~4*x^2 + ~4*x + 1]^2)))))") + + +text \One component of denominator in dodecahedral example.\ + +lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" + by (sos_cert "(((A<0 * R<1) + ((R<1 * ((R<5749028157/5000000000 * [~25000/222477*x + ~25000/222477*y + ~25000/222477*z + 1]^2) + ((R<864067/1779816 * [419113/864067*x + 419113/864067*y + z]^2) + ((R<320795/864067 * [419113/1283180*x + y]^2) + (R<1702293/5132720 * [x]^2))))) + (((A<=4 * (A<=5 * R<1)) * (R<3/2 * [1]^2)) + (((A<=3 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<3/2 * [1]^2)) + (((A<=1 * (A<=5 * R<1)) * (R<1/2 * [1]^2)) + (((A<=1 * (A<=3 * R<1)) * (R<1/2 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<3/2 * [1]^2)))))))))))))") + + +text \Over a larger but simpler interval.\ + +lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" + by (sos_cert "((R<1 + ((R<1 * ((R<1 * [~1/6*x + ~1/6*y + ~1/6*z + 1]^2) + ((R<1/18 * [~1/2*x + ~1/2*y + z]^2) + (R<1/24 * [~1*x + y]^2)))) + (((A<0 * R<1) * (R<1/12 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<1/6 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<1/6 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1/6 * [1]^2)))))))))))") + + +text \We can do 12. I think 12 is a sharp bound; see PP's certificate.\ + +lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" + by (sos_cert "(((A<0 * R<1) + (((A<=4 * R<1) * (R<2/3 * [1]^2)) + (((A<=4 * (A<=5 * R<1)) * (R<1 * [1]^2)) + (((A<=3 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * R<1) * (R<2/3 * [1]^2)) + (((A<=2 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=2 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=2 * (A<=3 * R<1)) * (R<1 * [1]^2)) + (((A<=1 * (A<=4 * R<1)) * (R<1/3 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * R<1) * (R<2/3 * [1]^2)) + (((A<=0 * (A<=5 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=4 * R<1)) * (R<8/3 * [1]^2)) + (((A<=0 * (A<=3 * R<1)) * (R<1/3 * [1]^2)) + (((A<=0 * (A<=2 * R<1)) * (R<8/3 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2))))))))))))))))))") + + +text \Inequality from sci.math (see "Leon-Sotelo, por favor").\ + +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" + by (sos_cert "(((A<0 * R<1) + (([1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") + +lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" + by (sos_cert "(((A<0 * R<1) + (([~1*x + ~1*y + 1] * A=0) + (R<1 * ((R<1 * [~1/2*x + ~1/2*y + 1]^2) + (R<3/4 * [~1*x + y]^2))))))") + +lemma "0 <= (x::real) & 0 <= y --> x * y * (x + y)^2 <= (x^2 + y^2)^2" + by (sos_cert "(((A<0 * R<1) + (R<1 * ((R<1 * [~1/2*x^2 + y^2 + ~1/2*x*y]^2) + (R<3/4 * [~1*x^2 + x*y]^2)))))") + +lemma "(0::real) <= a & 0 <= b & 0 <= c & c * (2 * a + b)^3/ 27 <= x \ c * a^2 * b <= x" + by (sos_cert "(((A<0 * R<1) + (((A<=3 * R<1) * (R<1 * [1]^2)) + (((A<=1 * (A<=2 * R<1)) * (R<1/27 * [~1*a + b]^2)) + ((A<=0 * (A<=2 * R<1)) * (R<8/27 * [~1*a + b]^2))))))") + +lemma "(0::real) < x --> 0 < 1 + x + x^2" + by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + +lemma "(0::real) <= x --> 0 < 1 + x + x^2" + by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + +lemma "(0::real) < 1 + x^2" + by (sos_cert "((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") + +lemma "(0::real) <= 1 + 2 * x + x^2" + by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [x + 1]^2))))") + +lemma "(0::real) < 1 + abs x" + by (sos_cert "((R<1 + (((A<=1 * R<1) * (R<1/2 * [1]^2)) + ((A<=0 * R<1) * (R<1/2 * [1]^2)))))") + +lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" + by (sos_cert "(((R<1 + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [x + 1]^2))))) & ((R<1 + (((A<0 * R<1) * (R<1 * [x + 1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))") + + +lemma "abs ((1::real) + x^2) = (1::real) + x^2" + by (sos_cert "(() & (((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<1 * R<1) * (R<1/2 * [1]^2))))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2)))))))") +lemma "(3::real) * x + 7 * a < 4 \ 3 < 2 * x \ a < 0" + by (sos_cert "((R<1 + (((A<1 * R<1) * (R<2 * [1]^2)) + (((A<0 * R<1) * (R<3 * [1]^2)) + ((A<=0 * R<1) * (R<14 * [1]^2))))))") + +lemma "(0::real) < x --> 1 < y --> y * x <= z --> x < z" + by (sos_cert "((((A<0 * A<1) * R<1) + (((A<=1 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2)))))") +lemma "(1::real) < x --> x^2 < y --> 1 < y" + by (sos_cert "((((A<0 * A<1) * R<1) + ((R<1 * ((R<1/10 * [~2*x + y + 1]^2) + (R<1/10 * [~1*x + y]^2))) + (((A<1 * R<1) * (R<1/2 * [1]^2)) + (((A<0 * R<1) * (R<1 * [x]^2)) + (((A<=0 * R<1) * ((R<1/10 * [x + 1]^2) + (R<1/10 * [x]^2))) + (((A<=0 * (A<1 * R<1)) * (R<1/5 * [1]^2)) + ((A<=0 * (A<0 * R<1)) * (R<1/5 * [1]^2)))))))))") +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" + by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") +lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" + by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") +lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" + by (sos_cert "(((A<0 * R<1) + (R<1 * (R<1 * [2*a*x + b]^2))))") +lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" + by (sos_cert "(((A<0 * (A<0 * R<1)) + (((A<=2 * (A<=3 * (A<0 * R<1))) * (R<2 * [1]^2)) + ((A<=0 * (A<=1 * R<1)) * (R<1 * [1]^2)))))") +lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" + by (sos_cert "((((A<0 * R<1) + (((A<=3 * (A<=6 * R<1)) * (R<1 * [1]^2)) + ((A<=1 * (A<=5 * R<1)) * (R<1 * [1]^2))))) & ((((A<0 * A<1) * R<1) + (((A<=3 * (A<=5 * (A<0 * R<1))) * (R<1 * [1]^2)) + ((A<=1 * (A<=4 * (A<0 * R<1))) * (R<1 * [1]^2))))))") + + +(* lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*) + +lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x" + by (sos_cert "(((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + ((A<0 * R<1) * (R<1 * [1]^2))))))") + +lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)" + by (sos_cert "(((R<1 + (([~4/3] * A=0) + ((R<1 * ((R<1/3 * [3/2*x + 1]^2) + (R<7/12 * [x]^2))) + ((A<=0 * R<1) * (R<1/3 * [1]^2)))))) & (((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2)))) & ((R<1 + ((R<1 * (R<1 * [x]^2)) + (((A<0 * R<1) * (R<1 * [1]^2)) + ((A<=0 * R<1) * (R<1 * [1]^2))))))))") + +lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)" + by (sos_cert "((((A<0 * A<1) * R<1) + ((A<=0 * (A<0 * R<1)) * (R<1 * [x]^2))))") + +lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" + by (sos_cert "((((((A<0 * A<1) * R<1) + ([~4] * A=0))) & ((((A<0 * A<1) * R<1) + ([4] * A=0)))) & (((((A<0 * A<1) * R<1) + ([4] * A=0))) & ((((A<0 * A<1) * R<1) + ([~4] * A=0)))))") + +end + diff -r fa50722ad6cb -r b5d27faef560 src/HOL/ex/SOS_Remote.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SOS_Remote.thy Mon Sep 22 21:31:45 2014 +0200 @@ -0,0 +1,37 @@ +(* Title: HOL/ex/SOS_Remote.thy + Author: Amine Chaieb, University of Cambridge + Author: Philipp Meyer, TU Muenchen + +Examples for Sum_of_Squares: remote CSDP server. +*) + +theory SOS_Remote +imports "~~/src/HOL/Library/Sum_of_Squares" +begin + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \ a < 0" + by (sos remote_csdp) + +lemma "a1 >= 0 & a2 >= 0 \ (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" + by (sos remote_csdp) + +lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" + by (sos remote_csdp) + +lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" + by (sos remote_csdp) + +lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" + by (sos remote_csdp) + +lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" + by (sos remote_csdp) + +lemma "(w^2 + x^2 + y^2 + z^2 = 1) --> (w + x + y + z)^2 <= (4::real)" + by (sos remote_csdp) + +lemma "(x::real) >= 1 & y >= 1 --> x * y >= x + y - 1" + by (sos remote_csdp) + +end + diff -r fa50722ad6cb -r b5d27faef560 src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Mon Sep 22 15:01:27 2014 +0200 +++ b/src/Pure/Syntax/lexicon.ML Mon Sep 22 21:31:45 2014 +0200 @@ -16,7 +16,6 @@ val scan_longid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_tid: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_nat: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list - val scan_int: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_float: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_hex: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list val scan_bin: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list @@ -25,7 +24,7 @@ val is_tid: string -> bool datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF + FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF datatype token = Token of token_kind * string * Position.range val str_of_token: token -> string val pos_of_token: token -> Position.T @@ -52,7 +51,7 @@ val read_variable: string -> indexname option val read_nat: string -> int option val read_int: string -> int option - val read_xnum: string -> {radix: int, leading_zeros: int, value: int} + val read_num: string -> {radix: int, leading_zeros: int, value: int} val read_float: string -> {mant: int, exp: int} val mark_class: string -> string val unmark_class: string -> string val mark_type: string -> string val unmark_type: string -> string @@ -99,9 +98,9 @@ val scan_nat = Scan.many1 (Symbol.is_digit o Symbol_Pos.symbol); val scan_float = scan_nat @@@ $$$ "." @@@ scan_nat; -val scan_int = $$$ "-" @@@ scan_nat || scan_nat; val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol); val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); +val scan_num = scan_hex || scan_bin || scan_nat; val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) []; val scan_var = $$$ "?" @@@ scan_id_nat; @@ -118,7 +117,7 @@ datatype token_kind = Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | - FloatSy | XNumSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; + FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF; datatype token = Token of token_kind * string * Position.range; @@ -151,7 +150,6 @@ ("tvar", TVarSy), ("num_token", NumSy), ("float_token", FloatSy), - ("xnum_token", XNumSy), ("str_token", StrSy), ("string_token", StringSy), ("cartouche", Cartouche)]; @@ -172,7 +170,6 @@ | TVarSy => Markup.tvar | NumSy => Markup.numeral | FloatSy => Markup.numeral - | XNumSy => Markup.numeral | StrSy => Markup.inner_string | StringSy => Markup.inner_string | Cartouche => Markup.inner_cartouche @@ -263,16 +260,12 @@ (if xids then $$$ "_" @@@ scan_id || scan_id else scan_id) || $$$ "_" @@@ $$$ "_"; - val scan_num_unsigned = scan_hex || scan_bin || scan_nat; - val scan_num_signed = scan_hex || scan_bin || scan_int; - val scan_val = scan_tvar >> token TVarSy || scan_var >> token VarSy || scan_tid >> token TFreeSy || scan_float >> token FloatSy || - scan_num_unsigned >> token NumSy || - $$$ "#" @@@ scan_num_signed >> token XNumSy || + scan_num >> token NumSy || scan_longid >> token LongIdentSy || scan_xid >> token IdentSy; @@ -378,7 +371,7 @@ end; -(* read_xnum: hex/bin/decimal *) +(* read_num: hex/bin/decimal *) local @@ -400,34 +393,30 @@ in -fun read_xnum str = +fun read_num str = let - val (sign, radix, digs) = - (case Symbol.explode (perhaps (try (unprefix "#")) str) of - "0" :: "x" :: cs => (1, 16, map remap_hex cs) - | "0" :: "b" :: cs => (1, 2, cs) - | "-" :: cs => (~1, 10, cs) - | cs => (1, 10, cs)); + val (radix, digs) = + (case Symbol.explode str of + "0" :: "x" :: cs => (16, map remap_hex cs) + | "0" :: "b" :: cs => (2, cs) + | cs => (10, cs)); in {radix = radix, leading_zeros = leading_zeros digs, - value = sign * #1 (Library.read_radix_int radix digs)} + value = #1 (Library.read_radix_int radix digs)} end; end; fun read_float str = let - val (sign, cs) = - (case Symbol.explode str of - "-" :: cs => (~1, cs) - | cs => (1, cs)); + val cs = Symbol.explode str; val (intpart, fracpart) = (case take_prefix Symbol.is_digit cs of (intpart, "." :: fracpart) => (intpart, fracpart) | _ => raise Fail "read_float"); in - {mant = sign * #1 (Library.read_int (intpart @ fracpart)), + {mant = #1 (Library.read_int (intpart @ fracpart)), exp = length fracpart} end; diff -r fa50722ad6cb -r b5d27faef560 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Mon Sep 22 15:01:27 2014 +0200 +++ b/src/Pure/pure_thy.ML Mon Sep 22 21:31:45 2014 +0200 @@ -70,8 +70,8 @@ (map (fn name => Binding.make (name, @{here})) (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", - "any", "prop'", "num_const", "float_const", "xnum_const", "num_position", - "float_position", "xnum_position", "index", "struct", "tid_position", + "any", "prop'", "num_const", "float_const", "num_position", + "float_position", "index", "struct", "tid_position", "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) @@ -142,10 +142,8 @@ ("_strip_positions", typ "'a", NoSyn), ("_position", typ "num_token => num_position", Delimfix "_"), ("_position", typ "float_token => float_position", Delimfix "_"), - ("_position", typ "xnum_token => xnum_position", Delimfix "_"), ("_constify", typ "num_position => num_const", Delimfix "_"), ("_constify", typ "float_position => float_const", Delimfix "_"), - ("_constify", typ "xnum_position => xnum_const", Delimfix "_"), ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"), ("_indexdefault", typ "index", Delimfix ""), ("_indexvar", typ "index", Delimfix "'\\"), diff -r fa50722ad6cb -r b5d27faef560 src/ZF/Bin.thy --- a/src/ZF/Bin.thy Mon Sep 22 15:01:27 2014 +0200 +++ b/src/ZF/Bin.thy Mon Sep 22 21:31:45 2014 +0200 @@ -101,10 +101,23 @@ NCons(bin_mult(v,w),0))" syntax - "_Int" :: "xnum_token => i" ("_") + "_Int0" :: i ("#()0") + "_Int1" :: i ("#()1") + "_Int2" :: i ("#()2") + "_Neg_Int1" :: i ("#-()1") + "_Neg_Int2" :: i ("#-()2") +translations + "#0" \ "CONST integ_of(CONST Pls)" + "#1" \ "CONST integ_of(CONST Pls BIT 1)" + "#2" \ "CONST integ_of(CONST Pls BIT 1 BIT 0)" + "#-1" \ "CONST integ_of(CONST Min)" + "#-2" \ "CONST integ_of(CONST Min BIT 0)" + +syntax + "_Int" :: "num_token => i" ("#_" 1000) + "_Neg_Int" :: "num_token => i" ("#-_" 1000) ML_file "Tools/numeral_syntax.ML" -setup Numeral_Syntax.setup declare bin.intros [simp,TC] diff -r fa50722ad6cb -r b5d27faef560 src/ZF/Tools/numeral_syntax.ML --- a/src/ZF/Tools/numeral_syntax.ML Mon Sep 22 15:01:27 2014 +0200 +++ b/src/ZF/Tools/numeral_syntax.ML Mon Sep 22 21:31:45 2014 +0200 @@ -8,7 +8,6 @@ sig val make_binary: int -> int list val dest_binary: int list -> int - val setup: theory -> theory end; structure Numeral_Syntax: NUMERAL_SYNTAX = @@ -21,6 +20,7 @@ | mk_bit _ = raise Fail "mk_bit"; fun dest_bit (Const (@{const_syntax zero}, _)) = 0 + | dest_bit (Const (@{const_syntax one}, _)) = 1 | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1 | dest_bit _ = raise Match; @@ -58,28 +58,34 @@ fun show_int t = let val rev_digs = bin_of t; - val (sign, zs) = + val (c, zs) = (case rev rev_digs of - ~1 :: bs => ("-", prefix_len (equal 1) bs) - | bs => ("", prefix_len (equal 0) bs)); + ~1 :: bs => (@{syntax_const "_Neg_Int"}, prefix_len (equal 1) bs) + | bs => (@{syntax_const "_Int"}, prefix_len (equal 0) bs)); val num = string_of_int (abs (dest_binary rev_digs)); - in - "#" ^ sign ^ implode (replicate zs "0") ^ num - end; + in (c, implode (replicate zs "0") ^ num) end; (* translation of integer constant tokens to and from binary *) -fun int_tr [t as Free (str, _)] = - Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_xnum str)) +fun int_tr [Free (s, _)] = + Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Lexicon.read_num s)) | int_tr ts = raise TERM ("int_tr", ts); -fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t) - | int_tr' _ = raise Match; - +fun neg_int_tr [Free (s, _)] = + Syntax.const @{const_syntax integ_of} $ mk_bin (~ (#value (Lexicon.read_num s))) + | neg_int_tr ts = raise TERM ("neg_int_tr", ts); -val setup = - Sign.parse_translation [(@{syntax_const "_Int"}, K int_tr)] #> - Sign.print_translation [(@{const_syntax integ_of}, K int_tr')]; +fun integ_of_tr' [t] = + let val (c, s) = show_int t + in Syntax.const c $ Syntax.free s end + | integ_of_tr' _ = raise Match; + +val _ = Theory.setup + (Sign.parse_translation + [(@{syntax_const "_Int"}, K int_tr), + (@{syntax_const "_Neg_Int"}, K neg_int_tr)] #> + Sign.print_translation + [(@{const_syntax integ_of}, K integ_of_tr')]); end;