# HG changeset patch # User haftmann # Date 1236757547 -3600 # Node ID 39acdf03154802189d3f83f91dbdcfb71f665250 # Parent 14f469e70eab89e0143db1736a9f87f5b610ba02 moved Decision_Procs examples to Decision_Procs/ex diff -r 14f469e70eab -r 39acdf031548 src/HOL/Decision_Procs/Decision_Procs.thy --- a/src/HOL/Decision_Procs/Decision_Procs.thy Wed Mar 11 08:45:46 2009 +0100 +++ b/src/HOL/Decision_Procs/Decision_Procs.thy Wed Mar 11 08:45:47 2009 +0100 @@ -1,5 +1,7 @@ +header {* Various decision procedures. typically involving reflection *} + theory Decision_Procs -imports Cooper Ferrack MIR Approximation Dense_Linear_Order +imports Cooper Ferrack MIR Approximation Dense_Linear_Order "ex/Approximation_Ex" "ex/Dense_Linear_Order_Ex" begin end \ No newline at end of file diff -r 14f469e70eab -r 39acdf031548 src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Wed Mar 11 08:45:47 2009 +0100 @@ -0,0 +1,52 @@ +(* Title: HOL/ex/ApproximationEx.thy + Author: Johannes Hoelzl 2009 +*) + +theory Approximation_Ex +imports Complex_Main "~~/src/HOL/Decision_Procs/Approximation" +begin + +text {* + +Here are some examples how to use the approximation method. + +The parameter passed to the method specifies the precision used by the computations, it is specified +as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This +interval is specified as a conjunction of the lower and upper bound. It must have the form +@{text "\ l\<^isub>1 \ x\<^isub>1 \ x\<^isub>1 \ u\<^isub>1 ; \ ; l\<^isub>n \ x\<^isub>n \ x\<^isub>n \ u\<^isub>n \ \ F"} where @{term F} is the formula, and +@{text "x\<^isub>1, \, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \, l\<^isub>n"} and the upper bounds +@{text "u\<^isub>1, \, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form +@{term "m * pow2 e"} to specify a exact floating point value. + +*} + +section "Compute some transcendental values" + +lemma "\ ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \ < inverse (2^51) " + by (approximation 80) + +lemma "\ exp 1.626 - 5.083499996273 \ < (inverse 10 ^ 10 :: real)" + by (approximation 80) + +lemma "\ sqrt 2 - 1.4142135623730951 \ < inverse 10 ^ 16" + by (approximation 80) + +lemma "\ pi - 3.1415926535897932385 \ < inverse 10 ^ 18" + by (approximation 80) + +section "Use variable ranges" + +lemma "0.5 \ x \ x \ 4.5 \ \ arctan x - 0.91 \ < 0.455" + by (approximation 10) + +lemma "0.49 \ x \ x \ 4.49 \ \ arctan x - 0.91 \ < 0.455" + by (approximation 20) + +lemma "1 * pow2 -1 \ x \ x \ 9 * pow2 -1 \ \ arctan x - 0.91 \ < 0.455" + by (approximation 10) + +lemma "0 \ x \ x \ 1 \ 0 \ sin x" + by (approximation 10) + +end + diff -r 14f469e70eab -r 39acdf031548 src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy Wed Mar 11 08:45:47 2009 +0100 @@ -0,0 +1,153 @@ +(* Author: Amine Chaieb, TU Muenchen *) + +header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} + +theory Dense_Linear_Order_Ex +imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" +begin + +lemma + "\(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \ x - y >0" + by ferrack + +lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" + by ferrack + +lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \ 0 )" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" + by ferrack + +lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" + by ferrack + +lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" + by ferrack + +lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" + by ferrack + +lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). + (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y. + (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" + by ferrack + +lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" + by ferrack + +lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" + by ferrack + +end diff -r 14f469e70eab -r 39acdf031548 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 11 08:45:46 2009 +0100 +++ b/src/HOL/IsaMakefile Wed Mar 11 08:45:47 2009 +0100 @@ -680,6 +680,8 @@ Decision_Procs/MIR.thy \ Decision_Procs/mir_tac.ML \ Decision_Procs/Decision_Procs.thy \ + Decision_Procs/ex/Dense_Linear_Order_Ex.thy \ + Decision_Procs/ex/Approximation_Ex.thy \ Decision_Procs/ROOT.ML @$(ISABELLE_TOOL) usedir $(OUT)/HOL Decision_Procs @@ -823,13 +825,13 @@ $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \ Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \ - ex/ApproximationEx.thy ex/Arith_Examples.thy \ + ex/Arith_Examples.thy \ ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \ ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \ ex/CodegenSML_Test.thy ex/Codegenerator.thy \ ex/Codegenerator_Pretty.thy ex/Coherent.thy \ ex/Commutative_RingEx.thy ex/Commutative_Ring_Complete.thy \ - ex/Dense_Linear_Order_Ex.thy ex/Efficient_Nat_examples.thy \ + ex/Efficient_Nat_examples.thy \ ex/Eval_Examples.thy ex/ExecutableContent.thy \ ex/Formal_Power_Series_Examples.thy ex/Fundefs.thy \ ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \ diff -r 14f469e70eab -r 39acdf031548 src/HOL/ex/ApproximationEx.thy --- a/src/HOL/ex/ApproximationEx.thy Wed Mar 11 08:45:46 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,52 +0,0 @@ -(* Title: HOL/ex/ApproximationEx.thy - Author: Johannes Hoelzl 2009 -*) - -theory ApproximationEx -imports "~~/src/HOL/Decision_Procs/Approximation" -begin - -text {* - -Here are some examples how to use the approximation method. - -The parameter passed to the method specifies the precision used by the computations, it is specified -as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This -interval is specified as a conjunction of the lower and upper bound. It must have the form -@{text "\ l\<^isub>1 \ x\<^isub>1 \ x\<^isub>1 \ u\<^isub>1 ; \ ; l\<^isub>n \ x\<^isub>n \ x\<^isub>n \ u\<^isub>n \ \ F"} where @{term F} is the formula, and -@{text "x\<^isub>1, \, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \, l\<^isub>n"} and the upper bounds -@{text "u\<^isub>1, \, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form -@{term "m * pow2 e"} to specify a exact floating point value. - -*} - -section "Compute some transcendental values" - -lemma "\ ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \ < inverse (2^51) " - by (approximation 80) - -lemma "\ exp 1.626 - 5.083499996273 \ < (inverse 10 ^ 10 :: real)" - by (approximation 80) - -lemma "\ sqrt 2 - 1.4142135623730951 \ < inverse 10 ^ 16" - by (approximation 80) - -lemma "\ pi - 3.1415926535897932385 \ < inverse 10 ^ 18" - by (approximation 80) - -section "Use variable ranges" - -lemma "0.5 \ x \ x \ 4.5 \ \ arctan x - 0.91 \ < 0.455" - by (approximation 10) - -lemma "0.49 \ x \ x \ 4.49 \ \ arctan x - 0.91 \ < 0.455" - by (approximation 20) - -lemma "1 * pow2 -1 \ x \ x \ 9 * pow2 -1 \ \ arctan x - 0.91 \ < 0.455" - by (approximation 10) - -lemma "0 \ x \ x \ 1 \ 0 \ sin x" - by (approximation 10) - -end - diff -r 14f469e70eab -r 39acdf031548 src/HOL/ex/Dense_Linear_Order_Ex.thy --- a/src/HOL/ex/Dense_Linear_Order_Ex.thy Wed Mar 11 08:45:46 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,153 +0,0 @@ -(* Author: Amine Chaieb, TU Muenchen *) - -header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} - -theory Dense_Linear_Order_Ex -imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main -begin - -lemma - "\(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \ x - y >0" - by ferrack - -lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). 4*x + 3*y <= 0 & 4*x + 3*y >= -1)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < 0. (EX (y::'a::{ordered_field,recpower,number_ring, division_by_zero}) > 0. 7*x + y > 0 & x - y <= 9)" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" - by ferrack - -lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \ 0 )" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < 10 | x > 20 | (EX y. y>= 0 & y <= 10 & x+y = 20)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y < 5* z & 5*y >= 7*z & x < 0" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + 7*y - 5* z < 0 & 5*y + 7*z + 3*x < 0" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (abs (5*x+3*y+z) <= 5*x+3*y+z & abs (5*x+3*y+z) >= - (5*x+3*y+z)) | (abs (5*x+3*y+z) >= 5*x+3*y+z & abs (5*x+3*y+z) <= - (5*x+3*y+z))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero})>0. (ALL y. (EX z. 13* abs z \ abs (12*y - x) & 5*x - 3*(abs y) <= 7*z))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs (4*x + 17) < 4 & (ALL y . abs (x*34 - 34*y - 9) \ 0 \ (EX z. 5*x - 3*abs y <= 7*z))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y > abs (23*x - 9). (ALL z > abs (3*y - 19* abs x). x+z > 2*y))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y< abs (3*x - 1). (ALL z >= (3*abs x - 1). abs (12*x - 13*y + 19*z) > abs (23*x) ))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). abs x < 100 & (ALL y > x. (EX z<2*y - x. 5*x - 3*y <= 7*z))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 7*x<3*y --> 5*y < 7*z --> z < 2*w --> 7*(2*w-x) > 2*y" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + abs (y - 8*x + z) <= 89" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. 5*x + 3*z - 17*w + 7* (y - 8*x + z) <= max y (7*z - x + w)" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (EX w >= (x+y+z). w <= abs x + abs y + abs z)" - by ferrack - -lemma "~(ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. 3* x + z*4 = 3*y & x + y < z & x> w & 3*x < w + y))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z w. abs (x-y) = (z-w) & z*1234 < 233*x & w ~= y)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. (ALL w >= abs (x+y+z). w >= abs x + abs y + abs z)" - by ferrack - -lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX w >= (x+y+z). w <= abs x + abs y + abs z))" - by ferrack - -lemma "EX z. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) < abs z. (EX y w. x< y & x < z & x> w & 3*x < w + y))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z. (ALL w. abs (x-y) = abs (z-w) --> z < x & w ~= y))" - by ferrack - -lemma "EX y. (ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) z. (ALL w >= 13*x - 4*z. (EX y. w >= abs x + abs y + z))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). - (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y. - (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" - by ferrack - -lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z w. min (5*x + 3*z) (17*w) + 5* abs (y - 8*x + z) <= max y (7*z - x + w)" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (y - x) < w)))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. (ALL z>19. y <= x + z & (EX w. abs (x + z) < w - y)))" - by ferrack - -lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (EX y. abs y ~= abs x & (ALL z> max x y. (EX w. w ~= y & w ~= z & 3*w - z >= x + y)))" - by ferrack - -end diff -r 14f469e70eab -r 39acdf031548 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Mar 11 08:45:46 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Mar 11 08:45:47 2009 +0100 @@ -60,7 +60,6 @@ "Code_Antiq", "Termination", "Coherent", - "Dense_Linear_Order_Ex", "PresburgerEx", "ReflectionEx", "BinEx",