--- 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
--- 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
--- 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 ***
--- 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 "\<dots>"} @{verbatim "''"} \\
@{syntax_def (inner) string_token} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
@{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} @{text "\<dots>"} @{verbatim "\<close>"} \\
@@ -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.
*}
--- 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 \<Longrightarrow> 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 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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 \<longrightarrow> 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 \<and> 3 < 2 * x \<longrightarrow> 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
--- 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
--- 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
*}
--- 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]
--- /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 \<Longrightarrow> a < 0"
+ by (sos csdp)
+
+lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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 \<open>One component of denominator in dodecahedral example.\<close>
+
+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 \<open>Over a larger but simpler interval.\<close>
+
+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 \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close>
+
+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 \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close>
+
+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 \<longrightarrow> 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 \<and> 3 < 2 * x \<longrightarrow> 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
+
--- /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 \<Longrightarrow> 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 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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 \<open>One component of denominator in dodecahedral example.\<close>
+
+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 \<open>Over a larger but simpler interval.\<close>
+
+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 \<open>We can do 12. I think 12 is a sharp bound; see PP's certificate.\<close>
+
+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 \<open>Inequality from sci.math (see "Leon-Sotelo, por favor").\<close>
+
+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 \<longrightarrow> 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 \<and> 3 < 2 * x \<longrightarrow> 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
+
--- /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 \<Longrightarrow> a < 0"
+ by (sos remote_csdp)
+
+lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (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
+
--- 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;
--- 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 "'\\<index>"),
--- 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" \<rightleftharpoons> "CONST integ_of(CONST Pls)"
+ "#1" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1)"
+ "#2" \<rightleftharpoons> "CONST integ_of(CONST Pls BIT 1 BIT 0)"
+ "#-1" \<rightleftharpoons> "CONST integ_of(CONST Min)"
+ "#-2" \<rightleftharpoons> "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]
--- 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;