src/HOL/ex/Dense_Linear_Order_Ex.thy
 author nipkow Fri Mar 06 17:38:47 2009 +0100 (2009-03-06) changeset 30313 b2441b0c8d38 parent 29823 0ab754d13ccd permissions -rw-r--r--
 haftmann@29823 ` 1` ```(* Author: Amine Chaieb, TU Muenchen *) ``` wenzelm@23454 ` 2` wenzelm@23454 ` 3` ```header {* Examples for Ferrante and Rackoff's quantifier elimination procedure *} ``` wenzelm@23454 ` 4` wenzelm@23454 ` 5` ```theory Dense_Linear_Order_Ex ``` haftmann@29823 ` 6` ```imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Main ``` wenzelm@23454 ` 7` ```begin ``` wenzelm@23454 ` 8` wenzelm@23454 ` 9` ```lemma ``` wenzelm@23454 ` 10` ``` "\(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \ x - y >0" ``` chaieb@23905 ` 11` ``` by ferrack ``` wenzelm@23454 ` 12` wenzelm@23454 ` 13` ```lemma "~ (ALL x (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). x < y --> 10*x < 11*y)" ``` chaieb@23905 ` 14` ``` by ferrack ``` wenzelm@23454 ` 15` wenzelm@23454 ` 16` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (10*(x + 5*y + -1) < 60*y)" ``` chaieb@23905 ` 17` ``` by ferrack ``` wenzelm@23454 ` 18` wenzelm@23454 ` 19` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x ~= y --> x < y" ``` chaieb@23905 ` 20` ``` by ferrack ``` wenzelm@23454 ` 21` wenzelm@23454 ` 22` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 10*x ~= 9*y & 10*x < y) --> x < y" ``` chaieb@23905 ` 23` ``` by ferrack ``` wenzelm@23454 ` 24` wenzelm@23454 ` 25` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (x ~= y & 5*x <= y) --> 500*x <= 100*y" ``` chaieb@23905 ` 26` ``` by ferrack ``` wenzelm@23454 ` 27` wenzelm@23454 ` 28` ```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)" ``` chaieb@23905 ` 29` ``` by ferrack ``` wenzelm@23454 ` 30` wenzelm@23454 ` 31` ```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)" ``` chaieb@23905 ` 32` ``` by ferrack ``` wenzelm@23454 ` 33` wenzelm@23454 ` 34` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (0 < x & x < 1) --> (ALL y > 1. x + y ~= 1)" ``` chaieb@23905 ` 35` ``` by ferrack ``` wenzelm@23454 ` 36` wenzelm@23454 ` 37` ```lemma "EX x. (ALL (y::'a::{ordered_field,recpower,number_ring, division_by_zero}). y < 2 --> 2*(y - x) \ 0 )" ``` chaieb@23905 ` 38` ``` by ferrack ``` wenzelm@23454 ` 39` wenzelm@23454 ` 40` ```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)" ``` chaieb@23905 ` 41` ``` by ferrack ``` wenzelm@23454 ` 42` wenzelm@23454 ` 43` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. x + y < z --> y >= z --> x < 0" ``` chaieb@23905 ` 44` ``` by ferrack ``` wenzelm@23454 ` 45` wenzelm@23454 ` 46` ```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" ``` chaieb@23905 ` 47` ``` by ferrack ``` wenzelm@23454 ` 48` wenzelm@23454 ` 49` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y z. abs (x + y) <= z --> (abs z = z)" ``` chaieb@23905 ` 50` ``` by ferrack ``` wenzelm@23454 ` 51` wenzelm@23454 ` 52` ```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" ``` chaieb@23905 ` 53` ``` by ferrack ``` wenzelm@23454 ` 54` wenzelm@23454 ` 55` ```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))" ``` chaieb@23905 ` 56` ``` by ferrack ``` wenzelm@23454 ` 57` wenzelm@23454 ` 58` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" ``` chaieb@23905 ` 59` ``` by ferrack ``` wenzelm@23454 ` 60` wenzelm@23454 ` 61` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. x < y --> (EX z>0. x+z = y)" ``` chaieb@23905 ` 62` ``` by ferrack ``` wenzelm@23454 ` 63` wenzelm@23454 ` 64` ```lemma "ALL (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (EX z>0. abs (x - y) <= z )" ``` chaieb@23905 ` 65` ``` by ferrack ``` wenzelm@23454 ` 66` wenzelm@23454 ` 67` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" ``` chaieb@23905 ` 68` ``` by ferrack ``` wenzelm@23454 ` 69` wenzelm@23454 ` 70` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z>=0. abs (3*x+7*y) <= 2*z + 1)" ``` chaieb@23905 ` 71` ``` by ferrack ``` wenzelm@23454 ` 72` wenzelm@23454 ` 73` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}) y. (ALL z<0. (z < x --> z <= y) & (z > y --> z >= x))" ``` chaieb@23905 ` 74` ``` by ferrack ``` wenzelm@23454 ` 75` wenzelm@23454 ` 76` ```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))" ``` chaieb@23905 ` 77` ``` by ferrack ``` wenzelm@23454 ` 78` wenzelm@23454 ` 79` ```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))" ``` chaieb@23905 ` 80` ``` by ferrack ``` wenzelm@23454 ` 81` wenzelm@23454 ` 82` ```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))" ``` chaieb@23905 ` 83` ``` by ferrack ``` wenzelm@23454 ` 84` wenzelm@23454 ` 85` ```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) ))" ``` chaieb@23905 ` 86` ``` by ferrack ``` wenzelm@23454 ` 87` wenzelm@23454 ` 88` ```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))" ``` chaieb@23905 ` 89` ``` by ferrack ``` wenzelm@23454 ` 90` wenzelm@23454 ` 91` ```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" ``` chaieb@23905 ` 92` ``` by ferrack ``` wenzelm@23454 ` 93` wenzelm@23454 ` 94` ```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" ``` chaieb@23905 ` 95` ``` by ferrack ``` wenzelm@23454 ` 96` wenzelm@23454 ` 97` ```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)" ``` chaieb@23905 ` 98` ``` by ferrack ``` wenzelm@23454 ` 99` wenzelm@23454 ` 100` ```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)" ``` chaieb@23905 ` 101` ``` by ferrack ``` wenzelm@23454 ` 102` wenzelm@23454 ` 103` ```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)" ``` chaieb@23905 ` 104` ``` by ferrack ``` wenzelm@23454 ` 105` wenzelm@23454 ` 106` ```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))" ``` chaieb@23905 ` 107` ``` by ferrack ``` wenzelm@23454 ` 108` wenzelm@23454 ` 109` ```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)" ``` chaieb@23905 ` 110` ``` by ferrack ``` wenzelm@23454 ` 111` wenzelm@23454 ` 112` ```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))" ``` chaieb@23905 ` 113` ``` by ferrack ``` wenzelm@23454 ` 114` wenzelm@23454 ` 115` ```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)" ``` chaieb@23905 ` 116` ``` by ferrack ``` wenzelm@23454 ` 117` wenzelm@23454 ` 118` ```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))" ``` chaieb@23905 ` 119` ``` by ferrack ``` wenzelm@23454 ` 120` wenzelm@23454 ` 121` ```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))" ``` chaieb@23905 ` 122` ``` by ferrack ``` wenzelm@23454 ` 123` wenzelm@23454 ` 124` ```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))" ``` chaieb@23905 ` 125` ``` by ferrack ``` wenzelm@23454 ` 126` wenzelm@23454 ` 127` ```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)))" ``` chaieb@23905 ` 128` ``` by ferrack ``` wenzelm@23454 ` 129` wenzelm@23454 ` 130` ```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))" ``` chaieb@23905 ` 131` ``` by ferrack ``` wenzelm@23454 ` 132` wenzelm@23454 ` 133` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y < x. (EX z > (x+y). ``` wenzelm@23454 ` 134` ``` (ALL w. 5*w + 10*x - z >= y --> w + 7*x + 3*z >= 2*y)))" ``` chaieb@23905 ` 135` ``` by ferrack ``` wenzelm@23454 ` 136` wenzelm@23454 ` 137` ```lemma "EX (x::'a::{ordered_field,recpower,number_ring, division_by_zero}). (ALL y. (EX z > y. ``` wenzelm@23454 ` 138` ``` (ALL w . w < 13 --> w + 10*x - z >= y --> 5*w + 7*x + 13*z >= 2*y)))" ``` chaieb@23905 ` 139` ``` by ferrack ``` wenzelm@23454 ` 140` wenzelm@23454 ` 141` ```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)" ``` chaieb@23905 ` 142` ``` by ferrack ``` wenzelm@23454 ` 143` wenzelm@23454 ` 144` ```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)))" ``` chaieb@23905 ` 145` ``` by ferrack ``` wenzelm@23454 ` 146` wenzelm@23454 ` 147` ```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)))" ``` chaieb@23905 ` 148` ``` by ferrack ``` wenzelm@23454 ` 149` wenzelm@23454 ` 150` ```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)))" ``` chaieb@23905 ` 151` ``` by ferrack ``` wenzelm@23454 ` 152` wenzelm@23454 ` 153` ```end ```