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