src/HOL/Decision_Procs/ex/Dense_Linear_Order_Ex.thy
author nipkow
Tue Feb 23 16:25:08 2016 +0100 (2016-02-23)
changeset 62390 842917225d56
parent 60540 b7b71952c194
permissions -rw-r--r--
more canonical names
haftmann@29823
     1
(* Author:     Amine Chaieb, TU Muenchen *)
wenzelm@23454
     2
wenzelm@60533
     3
section \<open>Examples for Ferrante and Rackoff's quantifier elimination procedure\<close>
wenzelm@23454
     4
wenzelm@23454
     5
theory Dense_Linear_Order_Ex
wenzelm@48480
     6
imports "../Dense_Linear_Order"
wenzelm@23454
     7
begin
wenzelm@23454
     8
wenzelm@60540
     9
lemma "\<exists>(y::'a::linordered_field) < 2. x + 3* y < 0 \<and> x - y > 0"
chaieb@23905
    10
  by ferrack
wenzelm@23454
    11
wenzelm@60540
    12
lemma "\<not> (\<forall>x (y::'a::linordered_field). x < y \<longrightarrow> 10 * x < 11 * y)"
chaieb@23905
    13
  by ferrack
wenzelm@23454
    14
wenzelm@60540
    15
lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> 10 * (x + 5 * y + -1) < 60 * y"
chaieb@23905
    16
  by ferrack
wenzelm@23454
    17
wenzelm@60540
    18
lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<longrightarrow> x < y"
chaieb@23905
    19
  by ferrack
wenzelm@23454
    20
wenzelm@60540
    21
lemma "\<exists>(x::'a::linordered_field) y. x \<noteq> y \<and> 10 * x \<noteq> 9 * y \<and> 10 * x < y \<longrightarrow> x < y"
chaieb@23905
    22
  by ferrack
wenzelm@23454
    23
wenzelm@60540
    24
lemma "\<forall>(x::'a::linordered_field) y. x \<noteq> y \<and> 5 * x \<le> y \<longrightarrow> 500 * x \<le> 100 * y"
chaieb@23905
    25
  by ferrack
wenzelm@23454
    26
wenzelm@60540
    27
lemma "\<forall>x::'a::linordered_field. \<exists>y::'a::linordered_field. 4 * x + 3 * y \<le> 0 \<and> 4 * x + 3 * y \<ge> -1"
wenzelm@60540
    28
  by ferrack
wenzelm@60540
    29
wenzelm@60540
    30
lemma "\<forall>(x::'a::linordered_field) < 0. \<exists>(y::'a::linordered_field) > 0. 7 * x + y > 0 \<and> x - y \<le> 9"
chaieb@23905
    31
  by ferrack
wenzelm@23454
    32
wenzelm@60540
    33
lemma "\<exists>x::'a::linordered_field. 0 < x \<and> x < 1 \<longrightarrow> (\<forall>y > 1. x + y \<noteq> 1)"
chaieb@23905
    34
  by ferrack
wenzelm@23454
    35
wenzelm@60540
    36
lemma "\<exists>x. \<forall>y::'a::linordered_field. y < 2 \<longrightarrow> 2 * (y - x) \<le> 0"
chaieb@23905
    37
  by ferrack
wenzelm@23454
    38
wenzelm@60540
    39
lemma "\<forall>x::'a::linordered_field. x < 10 \<or> x > 20 \<or> (\<exists>y. y \<ge> 0 \<and> y \<le> 10 \<and> x + y = 20)"
chaieb@23905
    40
  by ferrack
wenzelm@23454
    41
wenzelm@60540
    42
lemma "\<forall>(x::'a::linordered_field) y z. x + y < z \<longrightarrow> y \<ge> z \<longrightarrow> x < 0"
chaieb@23905
    43
  by ferrack
wenzelm@23454
    44
wenzelm@60540
    45
lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y < 5 * z \<and> 5 * y \<ge> 7 * z \<and> x < 0"
chaieb@23905
    46
  by ferrack
wenzelm@23454
    47
wenzelm@60540
    48
lemma "\<forall>(x::'a::linordered_field) y z. \<bar>x + y\<bar> \<le> z \<longrightarrow> \<bar>z\<bar> = z"
chaieb@23905
    49
  by ferrack
wenzelm@23454
    50
wenzelm@60540
    51
lemma "\<exists>(x::'a::linordered_field) y z. x + 7 * y - 5 * z < 0 \<and> 5 * y + 7 * z + 3 * x < 0"
chaieb@23905
    52
  by ferrack
wenzelm@23454
    53
wenzelm@60540
    54
lemma "\<forall>(x::'a::linordered_field) y z.
wenzelm@60540
    55
  (\<bar>5 * x + 3 * y + z\<bar> \<le> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<ge> - (5 * x + 3 * y + z)) \<or>
wenzelm@60540
    56
  (\<bar>5 * x + 3 * y + z\<bar> \<ge> 5 * x + 3 * y + z \<and> \<bar>5 * x + 3 * y + z\<bar> \<le> - (5 * x + 3 * y + z))"
chaieb@23905
    57
  by ferrack
wenzelm@23454
    58
wenzelm@60540
    59
lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)"
chaieb@23905
    60
  by ferrack
wenzelm@23454
    61
wenzelm@60540
    62
lemma "\<forall>(x::'a::linordered_field) y. x < y \<longrightarrow> (\<exists>z>0. x + z = y)"
chaieb@23905
    63
  by ferrack
wenzelm@23454
    64
wenzelm@60540
    65
lemma "\<forall>(x::'a::linordered_field) y. \<exists>z>0. \<bar>x - y\<bar> \<le> z"
chaieb@23905
    66
  by ferrack
wenzelm@23454
    67
wenzelm@60540
    68
lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)"
chaieb@23905
    69
  by ferrack
wenzelm@23454
    70
wenzelm@60540
    71
lemma "\<exists>(x::'a::linordered_field) y. \<forall>z\<ge>0. \<bar>3 * x + 7 * y\<bar> \<le> 2 * z + 1"
wenzelm@60540
    72
  by ferrack
wenzelm@60540
    73
wenzelm@60540
    74
lemma "\<exists>(x::'a::linordered_field) y. \<forall>z<0. (z < x \<longrightarrow> z \<le> y) \<and> (z > y \<longrightarrow> z \<ge> x)"
chaieb@23905
    75
  by ferrack
wenzelm@23454
    76
wenzelm@60540
    77
lemma "\<exists>(x::'a::linordered_field) > 0. \<forall>y. \<exists>z. 13 * \<bar>z\<bar> \<noteq> \<bar>12 * y - x\<bar> \<and> 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z"
chaieb@23905
    78
  by ferrack
wenzelm@23454
    79
wenzelm@60540
    80
lemma "\<exists>x::'a::linordered_field.
wenzelm@60540
    81
  \<bar>4 * x + 17\<bar> < 4 \<and> (\<forall>y. \<bar>x * 34 - 34 * y - 9\<bar> \<noteq> 0 \<longrightarrow> (\<exists>z. 5 * x - 3 * \<bar>y\<bar> \<le> 7 * z))"
chaieb@23905
    82
  by ferrack
wenzelm@23454
    83
wenzelm@60540
    84
lemma "\<forall>x::'a::linordered_field. \<exists>y > \<bar>23 * x - 9\<bar>. \<forall>z > \<bar>3 * y - 19 * \<bar>x\<bar>\<bar>. x + z > 2 * y"
chaieb@23905
    85
  by ferrack
wenzelm@23454
    86
wenzelm@60540
    87
lemma "\<forall>x::'a::linordered_field.
wenzelm@60540
    88
  \<exists>y < \<bar>3 * x - 1\<bar>. \<forall>z \<ge> 3 * \<bar>x\<bar> - 1. \<bar>12 * x - 13 * y + 19 * z\<bar> > \<bar>23 * x\<bar>"
chaieb@23905
    89
  by ferrack
wenzelm@23454
    90
wenzelm@60540
    91
lemma "\<exists>x::'a::linordered_field. \<bar>x\<bar> < 100 \<and> (\<forall>y > x. (\<exists>z < 2 * y - x. 5 * x - 3 * y \<le> 7 * z))"
chaieb@23905
    92
  by ferrack
wenzelm@23454
    93
wenzelm@60540
    94
lemma "\<forall>(x::'a::linordered_field) y z w.
wenzelm@60540
    95
  7 * x < 3 * y \<longrightarrow> 5 * y < 7 * z \<longrightarrow> z < 2 * w \<longrightarrow> 7 * (2 * w - x) > 2 * y"
chaieb@23905
    96
  by ferrack
wenzelm@23454
    97
wenzelm@60540
    98
lemma "\<exists>(x::'a::linordered_field) y z w. 5 * x + 3 * z - 17 * w + \<bar>y - 8 * x + z\<bar> \<le> 89"
chaieb@23905
    99
  by ferrack
wenzelm@23454
   100
wenzelm@60540
   101
lemma "\<exists>(x::'a::linordered_field) y z w.
wenzelm@60540
   102
  5 * x + 3 * z - 17 * w + 7 * (y - 8 * x + z) \<le> max y (7 * z - x + w)"
chaieb@23905
   103
  by ferrack
wenzelm@23454
   104
wenzelm@60540
   105
lemma "\<exists>(x::'a::linordered_field) y z w.
wenzelm@60540
   106
  min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
chaieb@23905
   107
  by ferrack
wenzelm@23454
   108
wenzelm@60540
   109
lemma "\<forall>(x::'a::linordered_field) y z. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
chaieb@23905
   110
  by ferrack
wenzelm@23454
   111
wenzelm@60540
   112
lemma "\<not> (\<forall>x::'a::linordered_field. \<exists>y z w.
wenzelm@60540
   113
  3 * x + z * 4 = 3 * y \<and> x + y < z \<and> x > w \<and> 3 * x < w + y)"
chaieb@23905
   114
  by ferrack
wenzelm@23454
   115
wenzelm@60540
   116
lemma "\<forall>(x::'a::linordered_field) y. \<exists>z w. \<bar>x - y\<bar> = z - w \<and> z * 1234 < 233 * x \<and> w \<noteq> y"
chaieb@23905
   117
  by ferrack
wenzelm@23454
   118
wenzelm@60540
   119
lemma "\<forall>x::'a::linordered_field. \<exists>y z w.
wenzelm@60540
   120
  min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
chaieb@23905
   121
  by ferrack
wenzelm@23454
   122
wenzelm@60540
   123
lemma "\<exists>(x::'a::linordered_field) y z. \<forall>w \<ge> \<bar>x + y + z\<bar>. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
chaieb@23905
   124
  by ferrack
wenzelm@23454
   125
wenzelm@60540
   126
lemma "\<exists>z. \<forall>(x::'a::linordered_field) y. \<exists>w \<ge> x + y + z. w \<le> \<bar>x\<bar> + \<bar>y\<bar> + \<bar>z\<bar>"
wenzelm@60540
   127
  by ferrack
wenzelm@60540
   128
wenzelm@60540
   129
lemma "\<exists>z. \<forall>(x::'a::linordered_field) < \<bar>z\<bar>. \<exists>y w. x < y \<and> x < z \<and> x > w \<and> 3 * x < w + y"
chaieb@23905
   130
  by ferrack
wenzelm@23454
   131
wenzelm@60540
   132
lemma "\<forall>(x::'a::linordered_field) y. \<exists>z. \<forall>w. \<bar>x - y\<bar> = \<bar>z - w\<bar> \<longrightarrow> z < x \<and> w \<noteq> y"
chaieb@23905
   133
  by ferrack
wenzelm@23454
   134
wenzelm@60540
   135
lemma "\<exists>y. \<forall>x::'a::linordered_field. \<exists>z w.
wenzelm@60540
   136
  min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
chaieb@23905
   137
  by ferrack
wenzelm@23454
   138
wenzelm@60540
   139
lemma "\<exists>(x::'a::linordered_field) z. \<forall>w \<ge> 13 * x - 4 * z. \<exists>y. w \<ge> \<bar>x\<bar> + \<bar>y\<bar> + z"
chaieb@23905
   140
  by ferrack
wenzelm@23454
   141
wenzelm@60540
   142
lemma "\<exists>x::'a::linordered_field. \<forall>y < x. \<exists>z > x + y.
wenzelm@60540
   143
  \<forall>w. 5 * w + 10 * x - z \<ge> y \<longrightarrow> w + 7 * x + 3 * z \<ge> 2 * y"
chaieb@23905
   144
  by ferrack
wenzelm@23454
   145
wenzelm@60540
   146
lemma "\<exists>x::'a::linordered_field. \<forall>y. \<exists>z > y.
wenzelm@60540
   147
  \<forall>w. w < 13 \<longrightarrow> w + 10 * x - z \<ge> y \<longrightarrow> 5 * w + 7 * x + 13 * z \<ge> 2 * y"
chaieb@23905
   148
  by ferrack
wenzelm@23454
   149
wenzelm@60540
   150
lemma "\<exists>(x::'a::linordered_field) y z w.
wenzelm@60540
   151
  min (5 * x + 3 * z) (17 * w) + 5 * \<bar>y - 8 * x + z\<bar> \<le> max y (7 * z - x + w)"
chaieb@23905
   152
  by ferrack
wenzelm@23454
   153
wenzelm@60540
   154
lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>y - x\<bar> < w)"
chaieb@23905
   155
  by ferrack
wenzelm@23454
   156
wenzelm@60540
   157
lemma "\<forall>x::'a::linordered_field. \<exists>y. \<forall>z>19. y \<le> x + z \<and> (\<exists>w. \<bar>x + z\<bar> < w - y)"
chaieb@23905
   158
  by ferrack
wenzelm@23454
   159
wenzelm@60540
   160
lemma "\<forall>x::'a::linordered_field. \<exists>y.
wenzelm@60540
   161
  \<bar>y\<bar> \<noteq> \<bar>x\<bar> \<and> (\<forall>z > max x y. \<exists>w. w \<noteq> y \<and> w \<noteq> z \<and> 3 * w - z \<ge> x + y)"
chaieb@23905
   162
  by ferrack
wenzelm@23454
   163
wenzelm@23454
   164
end