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--
added lemmas
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
  "\<exists>(y::'a::{ordered_field,recpower,number_ring, division_by_zero}) <2. x + 3* y < 0 \<and> 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) \<le> 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 \<noteq> 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) \<noteq> 0 \<longrightarrow> (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